Class de.uka.ilkd.key.proof.proverules.ProveRulesTest
|
99%
successful |
Failed tests
schiffl_lemma_2
java.lang.AssertionError at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.sequentChanged(BuiltInRuleAppIndex.java:149) at de.uka.ilkd.key.proof.RuleAppIndex.sequentChanged(RuleAppIndex.java:299) at de.uka.ilkd.key.proof.Goal.fireSequentChanged(Goal.java:225) at de.uka.ilkd.key.proof.Goal.setSequent(Goal.java:364) at de.uka.ilkd.key.rule.executor.javadl.NoFindTacletExecutor.apply(NoFindTacletExecutor.java:99) at de.uka.ilkd.key.rule.Taclet.apply(Taclet.java:935) at de.uka.ilkd.key.rule.TacletApp.execute(TacletApp.java:349) at de.uka.ilkd.key.proof.Goal.apply(Goal.java:613) at de.uka.ilkd.key.macros.scripts.CutCommand.execute(CutCommand.java:53) at de.uka.ilkd.key.macros.scripts.CutCommand.execute(CutCommand.java:18) at de.uka.ilkd.key.macros.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:148) at de.uka.ilkd.key.proof.proverules.ProveRulesTest.loadTacletProof(ProveRulesTest.java:72) at de.uka.ilkd.key.proof.proverules.ProveRulesTest.lambda$data$0(ProveRulesTest.java:144) at org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$0(DynamicTestTestDescriptor.java:53) at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131) at org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:167) at org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:184) at org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$1(DynamicTestTestDescriptor.java:61) at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptorCall.lambda$ofVoid$0(InvocationInterceptorChain.java:78) at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106) at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64) at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45) at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37) at org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:60) at org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:32) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141) at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138) at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95) at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35) at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:226) at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:204) at java.base/java.util.Optional.ifPresent(Optional.java:183) at org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.lambda$invokeTestMethod$1(TestFactoryTestDescriptor.java:108) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.invokeTestMethod(TestFactoryTestDescriptor.java:95) at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138) at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141) at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138) at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95) at java.base/java.util.ArrayList.forEach(ArrayList.java:1541) at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141) at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138) at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95) at java.base/java.util.ArrayList.forEach(ArrayList.java:1541) at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141) at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137) at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139) at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73) at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138) at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95) at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35) at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57) at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54) at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107) at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88) at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54) at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67) at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52) at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114) at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86) at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86) at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:110) at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:90) at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:85) at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.base/java.lang.reflect.Method.invoke(Method.java:566) at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36) at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24) at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33) at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94) at com.sun.proxy.$Proxy2.stop(Unknown Source) at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193) at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129) at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100) at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60) at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56) at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113) at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65) at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69) at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Tests
| Test | Method name | Duration | Result |
|---|---|---|---|
| powPositive | data()[100] | 3.110s | passed |
| powPositiveConcrete | data()[101] | 3.100s | passed |
| powGeq1Concrete | data()[102] | 3.104s | passed |
| pow2InIntLower | data()[103] | 3.099s | passed |
| pow2InIntUpper | data()[104] | 3.123s | passed |
| logSelfConcrete | data()[105] | 3.113s | passed |
| log1Concrete | data()[106] | 3.121s | passed |
| logProduct | data()[107] | 3.116s | passed |
| logTimesBaseConcrete | data()[108] | 3.115s | passed |
| logProdIdentity | data()[109] | 3.117s | passed |
| moduloByteIsInByte | data()[10] | 3.207s | passed |
| logProdIdentityConcrete | data()[110] | 3.112s | passed |
| logPowIdentity | data()[111] | 3.109s | passed |
| logPowIdentityConcrete | data()[112] | 3.080s | passed |
| logPositive | data()[113] | 3.107s | passed |
| logPositiveConcrete | data()[114] | 3.112s | passed |
| logMono | data()[115] | 3.112s | passed |
| logMonoConcrete | data()[116] | 3.102s | passed |
| powLogLess | data()[117] | 3.119s | passed |
| powLogMore2 | data()[118] | 3.121s | passed |
| logLessThanPow | data()[119] | 3.144s | passed |
| moduloCharIsInChar | data()[11] | 3.202s | passed |
| logLessThanPowConcrete | data()[120] | 3.095s | passed |
| logSqueeze | data()[121] | 3.101s | passed |
| ifthenelse_equals | data()[122] | 3.107s | passed |
| ifthenelse_equals_1 | data()[123] | 3.110s | passed |
| ifthenelse_equals_2 | data()[124] | 3.113s | passed |
| disjointWithSingleton1 | data()[125] | 3.112s | passed |
| disjointWithSingleton2 | data()[126] | 3.114s | passed |
| disjointArrayRanges | data()[127] | 3.130s | passed |
| disjointArrayRangeAllFields1 | data()[128] | 3.133s | passed |
| disjointArrayRangeAllFields2 | data()[129] | 3.116s | passed |
| div_unique1 | data()[12] | 3.331s | passed |
| seqSelfDefinition | data()[130] | 3.139s | passed |
| seqOutsideValue | data()[131] | 3.117s | passed |
| castedGetAny | data()[132] | 3.125s | passed |
| seqGetAlphaCast | data()[133] | 3.118s | passed |
| getOfSeqSingleton | data()[134] | 3.126s | passed |
| getOfSeqSingletonConcrete | data()[135] | 3.118s | passed |
| getOfSeqConcat | data()[136] | 3.117s | passed |
| getOfSeqSub | data()[137] | 3.123s | passed |
| getOfSeqReverse | data()[138] | 3.120s | passed |
| lenOfSeqEmpty | data()[139] | 3.122s | passed |
| div_unique2 | data()[13] | 3.230s | passed |
| lenOfSeqSingleton | data()[140] | 3.117s | passed |
| lenOfSeqConcat | data()[141] | 3.121s | passed |
| lenOfSeqSub | data()[142] | 3.120s | passed |
| lenOfSeqReverse | data()[143] | 3.113s | passed |
| equalityToSeqGetAndSeqLenLeft | data()[144] | 3.112s | passed |
| equalityToSeqGetAndSeqLenRight | data()[145] | 3.109s | passed |
| getOfSeqSingletonEQ | data()[146] | 3.107s | passed |
| getOfSeqConcatEQ | data()[147] | 3.113s | passed |
| getOfSeqSubEQ | data()[148] | 3.103s | passed |
| getOfSeqReverseEQ | data()[149] | 3.118s | passed |
| div_exists | data()[14] | 3.305s | passed |
| lenOfSeqEmptyEQ | data()[150] | 3.114s | passed |
| lenOfSeqSingletonEQ | data()[151] | 3.155s | passed |
| lenOfSeqConcatEQ | data()[152] | 3.111s | passed |
| lenOfSeqSubEQ | data()[153] | 3.110s | passed |
| lenOfSeqReverseEQ | data()[154] | 3.111s | passed |
| getOfSeqDefEQ | data()[155] | 3.112s | passed |
| lenOfSeqDefEQ | data()[156] | 3.109s | passed |
| seqConcatWithSeqEmpty1 | data()[157] | 3.104s | passed |
| seqConcatWithSeqEmpty2 | data()[158] | 3.132s | passed |
| seqReverseOfSeqEmpty | data()[159] | 3.114s | passed |
| div_one | data()[15] | 3.174s | passed |
| subSeqComplete | data()[160] | 3.114s | passed |
| subSeqTailR | data()[161] | 3.112s | passed |
| subSeqTailL | data()[162] | 3.119s | passed |
| subSeqTailEQR | data()[163] | 3.147s | passed |
| subSeqTailEQL | data()[164] | 3.122s | passed |
| seqDef_split | data()[165] | 3.128s | passed |
| seqDef_induction_upper | data()[166] | 3.124s | passed |
| seqDef_induction_upper_concrete | data()[167] | 3.156s | passed |
| seqDef_induction_lower | data()[168] | 3.131s | passed |
| seqDef_induction_lower_concrete | data()[169] | 3.146s | passed |
| jdiv_one | data()[16] | 3.179s | passed |
| seqDef_split_in_three | data()[170] | 3.188s | passed |
| seqDef_empty | data()[171] | 3.119s | passed |
| seqDef_one_summand | data()[172] | 3.112s | passed |
| seqDef_lower_equals_upper | data()[173] | 3.142s | passed |
| seqDefOfSeq | data()[174] | 3.134s | passed |
| seqSelfDefinitionEQ2 | data()[175] | 3.131s | passed |
| indexOfSeqSingleton | data()[176] | 3.140s | passed |
| indexOfSeqConcatFirst | data()[177] | 3.124s | passed |
| indexOfSeqConcatSecond | data()[178] | 3.123s | passed |
| indexOfSeqSub | data()[179] | 3.141s | passed |
| div_zero | data()[17] | 3.214s | passed |
| lenOfArray2seq | data()[180] | 3.109s | passed |
| getAnyOfArray2seq | data()[181] | 3.122s | passed |
| getOfArray2seq | data()[182] | 3.117s | passed |
| getAnyOfNPermInv | data()[183] | 3.108s | passed |
| seqNPermRange | data()[184] | 3.173s | passed |
| seqPermTrans | data()[185] | 3.142s | passed |
| seqPermRefl | data()[186] | 3.136s | passed |
| seqPermSplit | data()[187] | 3.107s | passed |
| seqNPermRight | data()[188] | 3.199s | passed |
| seqPermFromSwap | data()[189] | 3.146s | passed |
| divResZero1 | data()[18] | 3.162s | passed |
| seqPermTransAlt0 | data()[190] | 3.139s | passed |
| seqPermTransAlt1 | data()[191] | 3.111s | passed |
| seqPermTransAlt2 | data()[192] | 3.123s | passed |
| seqPermTransAlt3 | data()[193] | 3.106s | passed |
| seqPermForall | data()[194] | 3.231s | passed |
| seqPermExists | data()[195] | 3.190s | passed |
| schiffl_lemma_2 | data()[196] | 4.190s | failed |
| schiffl_thm_1 | data()[197] | 3.902s | passed |
| eqSameSeq | data()[198] | 3.242s | passed |
| divResZero2 | data()[19] | 3.147s | passed |
| eqTermCut | data()[1] | 3.792s | passed |
| divResOne1 | data()[20] | 3.139s | passed |
| divResOne2 | data()[21] | 3.151s | passed |
| div_cancel1 | data()[22] | 3.174s | passed |
| div_cancel2 | data()[23] | 3.167s | passed |
| divAddMultDenom | data()[24] | 3.156s | passed |
| divMinus | data()[25] | 3.224s | passed |
| divMinusDenom | data()[26] | 3.171s | passed |
| divLeastDPos | data()[27] | 3.132s | passed |
| divLeastDNeg | data()[28] | 3.131s | passed |
| divGreatestDPos | data()[29] | 3.131s | passed |
| equivAllRight | data()[2] | 3.524s | passed |
| divGreatestDNeg | data()[30] | 3.105s | passed |
| divIncreasingPos | data()[31] | 3.154s | passed |
| divIncreasingNeg | data()[32] | 3.131s | passed |
| jdiv_zero | data()[33] | 3.142s | passed |
| jdivPulloutMinusNum | data()[34] | 3.156s | passed |
| jdivPulloutMinusDenom | data()[35] | 3.208s | passed |
| jdiv_uniquePosPos | data()[36] | 3.132s | passed |
| jdiv_uniquePosNeg | data()[37] | 3.131s | passed |
| jdiv_uniqueNegPos | data()[38] | 3.132s | passed |
| jdiv_uniqueNegNeg | data()[39] | 3.127s | passed |
| irrflConcrete1 | data()[3] | 3.458s | passed |
| jdivMultDenom1 | data()[40] | 3.158s | passed |
| jdivMultDenom2 | data()[41] | 3.124s | passed |
| mod_geZero | data()[42] | 3.120s | passed |
| mod_lessDenom | data()[43] | 3.125s | passed |
| jmod_NumPos | data()[44] | 3.143s | passed |
| jmod_NumNeg | data()[45] | 3.166s | passed |
| jmod_geZero | data()[46] | 3.130s | passed |
| jmodNumZero | data()[47] | 3.144s | passed |
| jmod_pulloutminusNum | data()[48] | 3.137s | passed |
| jmod_pulloutminusDenom | data()[49] | 3.119s | passed |
| irrflConcrete2 | data()[4] | 3.460s | passed |
| jmodUnique1 | data()[50] | 3.182s | passed |
| jmodUnique2 | data()[51] | 3.162s | passed |
| intDivRem | data()[52] | 3.120s | passed |
| jmodjmod | data()[53] | 3.126s | passed |
| jmodDivisible | data()[54] | 3.141s | passed |
| jmodDivisibleRep | data()[55] | 3.152s | passed |
| jdivAddMultDenom | data()[56] | 3.202s | passed |
| jmodAltZero | data()[57] | 3.149s | passed |
| jmodAddMultDenomZero | data()[58] | 3.130s | passed |
| polyDiv_zero | data()[59] | 3.118s | passed |
| cancel_gtPos | data()[5] | 3.284s | passed |
| polyMod_ltdivDenom | data()[60] | 3.114s | passed |
| bsum_empty | data()[61] | 3.114s | passed |
| bsum_induction_upper | data()[62] | 3.111s | passed |
| bsum_induction_lower | data()[63] | 3.125s | passed |
| bsum_num_of_bounds | data()[64] | 3.135s | passed |
| bsum_num_of_bounds2 | data()[65] | 3.199s | passed |
| bsum_induction_upper2 | data()[66] | 3.133s | passed |
| bsum_induction_upper_concrete | data()[67] | 3.124s | passed |
| bsum_induction_upper_concrete_2 | data()[68] | 3.137s | passed |
| bsum_induction_upper2_concrete | data()[69] | 3.157s | passed |
| cancel_gtNeg | data()[6] | 3.383s | passed |
| bsum_induction_lower_concrete | data()[70] | 3.118s | passed |
| bsum_induction_lower2 | data()[71] | 3.106s | passed |
| bsum_induction_lower2_concrete | data()[72] | 3.129s | passed |
| bsum_positive | data()[73] | 3.156s | passed |
| bsum_upper_bound | data()[74] | 3.169s | passed |
| bsum_lower_bound | data()[75] | 3.169s | passed |
| bsum_positive_lower_bound_element | data()[76] | 3.163s | passed |
| bsum_sub_same_index | data()[77] | 3.136s | passed |
| bsum_less_same_index | data()[78] | 3.151s | passed |
| bsum_equal_except_one_index | data()[79] | 3.161s | passed |
| moduloIntIsInInt | data()[7] | 3.256s | passed |
| bsum_num_of_is_max | data()[80] | 3.138s | passed |
| bsum_num_of_is_max2 | data()[81] | 3.145s | passed |
| bsum_num_of_is_max3 | data()[82] | 3.140s | passed |
| bsum_num_of_is_max4 | data()[83] | 3.133s | passed |
| bsum_num_of_lt_max | data()[84] | 3.133s | passed |
| bsum_num_of_lt_max2 | data()[85] | 3.140s | passed |
| bsum_num_of_lt_max3 | data()[86] | 3.130s | passed |
| bsum_num_of_lt_max4 | data()[87] | 3.119s | passed |
| bsum_num_of_gt0 | data()[88] | 3.143s | passed |
| bsum_num_of_gt0_alt | data()[89] | 3.133s | passed |
| moduloLongIsInLong | data()[8] | 3.212s | passed |
| bsum_add_concrete | data()[90] | 3.121s | passed |
| bprod_all_positive | data()[91] | 3.131s | passed |
| bprod_split | data()[92] | 3.127s | passed |
| powConcrete0 | data()[93] | 3.096s | passed |
| powConcrete1 | data()[94] | 3.109s | passed |
| powSplitFactor | data()[95] | 3.112s | passed |
| powAdd | data()[96] | 3.105s | passed |
| powMono | data()[97] | 3.115s | passed |
| powMonoConcrete | data()[98] | 3.104s | passed |
| powMonoConcreteRight | data()[99] | 3.103s | passed |
| moduloShortIsInShort | data()[9] | 3.215s | passed |
Standard output
635 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file src/test/resources/testcase/dummyTrue.key 871 WARN Test worker 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) 878 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/standardRules.key 904 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 908 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/boolean.key 919 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key 954 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerHeader.key 961 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatHeader.key 964 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heap.key 967 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSets.key 968 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permission.key 970 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reach.key 971 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seq.key 972 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/map.key 1010 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/freeADT.key 1012 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wellfound.key 1013 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListHeader.key 1120 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/propRule.key 1144 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/firstOrderRules.key 1173 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ifThenElseRules.key 1229 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key 1322 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/updateRules.key 1352 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerRulesCommon.key 1460 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRules.key 1511 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key 1521 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key 1526 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key 1538 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key 1754 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1755 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1757 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1758 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1784 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intDiv.key 1857 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bsum.key 2032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bprod.key 2119 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryAxioms.key 2124 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryLemmas.key 2136 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intPow.key 2158 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesCommon.key 2185 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRules.key 2186 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key 2187 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key 2225 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/genericRules.key 2243 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/booleanRules.key 2248 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/epsilon.key 2251 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSetsRules.key 2307 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heapRules.key 2364 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permissionRules.key 2410 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reachRules.key 2439 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqCoreRules.key 2442 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqRules.key 2481 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm.key 2510 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm2.key 2516 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/javaRules.key 2617 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/assertions.key 3060 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopRules.key 3069 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/activeUse.key 3103 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/instanceAllocation.key 3117 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/java5.key 3120 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key 3145 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key 3164 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bigint.key 3173 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression 3175 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key 3191 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/precRules.key 3193 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListRules.key 3231 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExTheory.key 3232 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExHeader.key 3232 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExAxioms.key 3236 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExLemmaProven.key 3242 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqEq.key 3250 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/infFlow.key 3257 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/mapSize.key 3260 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wd.key 3261 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeader.key 3262 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdGeneralRules.key 3266 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdNumericalRules.key 3291 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdLocSetRules.key 3298 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeapRules.key 3302 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdReachRules.key 3304 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdSeqRules.key 3308 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdStringRules.key 3311 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdRegExRules.key 3313 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdFormulaRules.key 3329 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopInvariantRules.key 3331 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/forLoopRules.key 3333 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/execRules.key 3397 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopScopeRules.key 6275 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 8566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.61ns 8568 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file src/test/resources/testcase/dummyTrue.key 8581 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 9542 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 11422 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 12362 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.93ms 12363 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 12378 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 13282 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 15069 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 15899 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 15899 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 15901 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 16732 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 18502 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 19357 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 19357 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 19361 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 20184 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 21969 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 22818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 22819 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 22821 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 23575 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 25264 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 26104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.04ms 26104 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 26119 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 26903 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 28675 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 29496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 29497 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 29501 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 30254 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 31949 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 32754 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.03ns 32754 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 32757 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 33510 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 35171 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 35966 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.42ns 35967 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 35969 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 36717 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 38401 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 39178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 39179 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 39184 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 39963 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 41618 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 42388 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 42388 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 42393 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 43172 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 44819 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 45592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.63ns 45593 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 45595 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 46371 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 48082 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 48918 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.42ms 48924 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 48928 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 49704 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 51341 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 52152 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.32ms 52155 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 52158 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 52939 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 54574 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 55460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 119.73ms 55460 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 55463 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 56227 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 57874 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 58634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 58634 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 58636 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 59397 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 61005 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 61813 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 61813 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 61815 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 62580 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 64184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 65024 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.93ms 65025 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 65032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 65799 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 67403 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 68190 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 68190 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 68192 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 68953 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 70549 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 71337 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms 71338 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 71339 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 72098 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 73691 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 74476 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 74476 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 74478 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 75238 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 76840 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 77627 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 77627 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 77629 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 78386 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 79988 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 80801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ms 80801 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 80803 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 81573 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 83180 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 83968 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 83968 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 83970 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 84703 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 86322 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 87124 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 87125 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 87126 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 87861 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 89489 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 90344 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.09ms 90346 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 90352 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 91093 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 92718 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 93521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 93521 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 93524 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 94259 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 95876 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 96653 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 96653 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 96654 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 97385 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 99004 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 99784 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 99784 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 99785 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 100518 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 102136 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 102915 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 102916 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 102917 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 103647 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 105265 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 106020 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 106021 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 106022 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 106794 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 108419 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 109174 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 109174 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 109177 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 109934 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 111550 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 112305 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 112306 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 112307 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 113074 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 114698 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 115448 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 115448 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 115449 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 116204 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 117832 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 118599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.89ms 118602 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 118606 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 119373 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 121029 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 121811 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.63ms 121811 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 121813 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 122570 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 124158 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 124943 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 124944 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 124945 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 125698 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 127285 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 128074 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 128074 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 128075 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 128830 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 130419 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 131206 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 131206 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 131207 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 131961 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 133550 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 134333 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 134333 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 134335 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 135093 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 136688 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 137491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.34ms 137491 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 137493 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 138249 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 139843 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 140615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 140615 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 140616 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 141370 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 142962 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 143735 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 143735 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 143737 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 144491 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 146082 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 146860 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 146860 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 146861 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 147622 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 149211 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 150002 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.04ms 150003 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 150005 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 150751 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 152375 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 153170 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.12ms 153170 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 153171 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 153904 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 155516 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 156298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 156299 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 156301 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 157030 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 158648 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 159442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 159443 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 159445 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 160177 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 161801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 162579 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 162580 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 162582 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 163310 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 164928 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 165698 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 165699 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 165701 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 166431 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 168048 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 168879 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.74ms 168880 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 168883 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 169612 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 171226 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 172043 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.49ms 172043 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 172045 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 172804 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 174417 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 175163 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 175163 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 175165 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 175914 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 177518 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 178289 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.41ms 178289 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 178291 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 179055 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 180664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 181430 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms 181430 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 181431 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 182185 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 183809 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 184582 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.82ns 184582 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 184584 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 185336 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 186942 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 187784 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.34ms 187784 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 187788 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 188554 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 190178 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 190933 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 190934 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 190936 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 191701 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 193288 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 194064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 194064 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 194065 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 194817 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 196402 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 197182 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 197182 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 197184 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 197935 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 199518 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 200295 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 200297 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 200298 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 201057 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 202639 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 203410 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 203411 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 203412 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 204159 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 205749 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 206521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 206521 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 206522 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 207276 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 208865 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 209646 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.34ms 209646 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 209648 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 210403 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 211993 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 212781 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms 212782 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 212783 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 213601 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 215197 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 215980 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 215980 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 215982 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 216725 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 218343 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 219113 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 219113 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 219115 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 219842 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 221462 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 222238 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 222238 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 222239 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 222969 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 224599 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 225374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 225374 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 225375 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 226107 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 227750 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 228531 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.82ns 228531 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 228532 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 229261 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 230880 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 231649 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.91ns 231649 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 231651 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 232379 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 234004 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 234756 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 234756 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 234757 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 235513 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 237131 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 237884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.41ns 237885 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 237886 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 238642 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 240256 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 241039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.75ms 241040 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 241042 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 241809 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 243435 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 244209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.45ms 244209 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 244211 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 244963 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 246594 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 247373 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.86ms 247378 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 247381 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 248147 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 249769 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 250541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.99ms 250541 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 250542 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 251296 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 252913 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 253677 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.36ms 253678 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 253679 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 254436 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 256021 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 256828 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.89ms 256828 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 256829 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 257595 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 259194 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 259988 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 259989 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 259991 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 260747 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 262344 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 263127 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.72ms 263127 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 263129 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 263881 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 265483 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 266273 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.01ms 266273 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 266274 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 267028 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 268628 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 269412 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.62ms 269412 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 269414 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 270169 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 271756 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 272544 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 272545 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 272547 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 273307 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 274893 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 275678 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 275679 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 275680 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 276439 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 278033 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 278818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 278818 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 278820 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 279577 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 281164 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 281947 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.47ms 281948 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 281950 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 282677 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 284283 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 285066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 285067 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 285069 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 285797 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 287428 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 288210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 288210 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 288212 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 288942 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 290560 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 291343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 291343 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 291345 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 292072 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 293690 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 294464 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 294464 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 294465 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 295192 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 296813 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 297596 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 297596 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 297597 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 298327 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 299951 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 300723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 300723 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 300724 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 301450 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 303068 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 303818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.91ns 303819 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 303820 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 304577 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 306180 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 306928 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.21ns 306928 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 306929 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 307687 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 309289 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 310039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 310039 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 310041 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 310790 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 312395 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 313145 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 313145 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 313146 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 313896 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 315504 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 316259 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 316259 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 316260 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 317011 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 318617 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 319363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 319364 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 319365 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 320115 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 321695 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 322466 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 456.51ns 322466 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 322468 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 323220 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 324804 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 325577 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 325577 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 325578 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 326326 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 327906 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 328675 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.11ns 328677 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 328678 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 329430 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 331010 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 331780 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.71ns 331780 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 331781 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 332529 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 334110 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 334879 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555ns 334880 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 334882 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 335638 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 337232 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 338003 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 338003 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 338004 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 338756 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 340341 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 341115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 341115 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 341117 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 341879 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 343464 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 344236 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 344236 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 344237 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 344963 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 346577 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 347353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 347353 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 347354 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 348080 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 349692 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 350467 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 350467 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 350469 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 351196 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 352805 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 353584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 353584 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 353586 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 354309 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 355927 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 356697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 356697 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 356698 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 357423 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 359032 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 359805 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 359805 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 359807 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 360532 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 362139 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 362886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 362886 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 362887 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 363632 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 365235 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 365992 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 365992 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 365993 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 366747 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 368358 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 369103 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 295.8ns 369104 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 369106 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 369853 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 371444 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 372215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.85ms 372216 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 372218 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 372966 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 374571 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 375318 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 375319 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 375320 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 376068 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 377672 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 378436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.99ms 378437 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 378439 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 379198 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 380779 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 381558 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 381558 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 381560 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 382308 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 383908 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 384702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.98ms 384703 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 384704 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 385451 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 387028 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 387797 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.11ns 387797 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 387798 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 388546 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 390125 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 390897 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 390898 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 390900 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 391650 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 393229 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 394006 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 394006 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 394007 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 394757 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 396337 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 397115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.91ns 397116 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 397117 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 397868 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 399453 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 400228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.91ns 400228 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 400230 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 400977 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 402562 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 403340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 403340 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 403342 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 404096 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 405679 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 406455 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 406455 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 406457 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 407184 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 408805 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 409585 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 409585 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 409586 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 410314 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 411937 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 412718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 412718 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 412719 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 413443 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 415055 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 415834 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 415835 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 415836 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 416561 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 418182 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 418973 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 418973 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 418974 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 419699 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 421303 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 422090 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 422090 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 422091 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 422819 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 424432 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 425215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 425215 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 425216 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 425940 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 427550 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 428334 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 834.81ns 428334 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 428335 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 429061 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 430671 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 431459 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 431459 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 431460 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 432183 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 433794 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 434578 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.21ns 434578 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 434579 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 435303 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 436906 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 437694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 437694 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 437696 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 438421 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 440034 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 440817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 440817 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 440819 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 441544 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 443151 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 443937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 443938 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 443939 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 444666 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 446277 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 447060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 810.31ns 447060 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 447061 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 447784 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 449393 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 450176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.31ns 450176 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 450177 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 450902 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 452510 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 453297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 453297 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 453298 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 454024 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 455635 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 456417 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.21ns 456417 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 456418 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 457142 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 458747 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 459530 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.21ns 459530 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 459533 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 460259 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 461861 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 462643 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.4ns 462643 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 462644 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 463394 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 464968 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 465751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 465751 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 465752 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 466499 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 468076 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 468858 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 821.01ns 468858 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 468860 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 469608 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 471184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 471971 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 471971 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 471973 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 472720 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 474294 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 475074 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 507.11ns 475074 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 475075 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 475825 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 477428 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 478192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 478192 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 478193 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 478944 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 480548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 481307 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.41ns 481307 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 481308 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 482079 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 483679 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 484462 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.41ns 484462 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 484463 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 485186 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 486789 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 487572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 487572 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 487574 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 488297 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 489902 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 490683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.61ns 490683 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 490684 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 491434 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 493009 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 493793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 493794 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 493795 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 494543 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 496119 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 496905 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 496905 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 496906 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 497655 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 499254 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 500014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 500014 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 500015 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 500762 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 502356 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 503119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 503119 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 503120 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 503866 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 505464 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 506251 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 506251 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 506252 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 506976 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 508580 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 509364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 509364 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 509366 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 510117 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 511694 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 512478 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 512478 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 512479 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 513227 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 514800 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 515590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 515590 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 515592 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 516339 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 517943 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 518709 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 518709 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 518710 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 519470 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 521067 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 521856 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.14ms 521856 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 521857 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 522583 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 524191 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 524978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 524978 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 524980 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 525728 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 527305 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 528106 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.14ms 528106 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 528108 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 528854 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 530452 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 531230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.41ms 531231 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 531232 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 531980 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 533586 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 534386 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 534387 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 534388 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 535139 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 536716 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 537517 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 537517 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 537519 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 538270 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 539885 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 540663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ms 540663 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 540664 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 541416 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 543025 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 543851 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.76ms 543851 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 543852 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 544578 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 546181 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 546969 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 546969 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 546971 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 547720 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 549298 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 550083 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 550083 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 550084 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 550832 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 552439 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 553224 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 553224 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 553225 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 553953 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 555559 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 556358 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 556358 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 556360 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 557112 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 558698 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 559490 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 559490 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 559491 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 560239 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 561845 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 562630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 562630 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 562631 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 563356 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 564960 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 565753 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 565753 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 565755 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 566503 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 568109 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 568876 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.62ms 568877 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 568878 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 569624 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 571221 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 572018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.01ms 572018 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 572019 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 572767 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 574344 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 575127 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.59ns 575127 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 575128 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 575873 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 577468 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 578248 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 578248 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 578249 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 578973 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 580580 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 581365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 581365 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 581367 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 582112 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 583712 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 584474 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 584474 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 584475 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 585224 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 586825 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 587646 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.51ms 587647 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 587648 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 588396 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 589982 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 590788 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.62ms 590788 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 590790 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 591537 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 593134 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 593924 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 593924 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 593925 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 594669 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 596246 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 597031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 293.5ns 597031 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 597033 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 597779 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 599377 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 600230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.88ms 600230 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 600232 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 600979 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 602560 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 603376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.92ms 603377 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 603379 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 604131 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 605735 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 606516 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 205ns 606516 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 606517 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 607262 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 608839 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 609625 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.7ns 609626 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 609628 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 610372 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 611966 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 612749 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.3ns 612749 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 612751 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 613497 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 615073 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 615855 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.8ns 615855 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 615857 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 616601 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 618198 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 619080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.69ms 619086 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 619088 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 619847 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 621460 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 622276 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.16ms 622276 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 622278 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 623038 DEBUG Test worker d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 623040 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 624656 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 625440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 625440 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 625466 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 625526 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 625542 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 625548 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 625564 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 625565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 625567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 625569 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 625576 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange' 625577 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 625582 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 625584 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 625808 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 625809 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 625811 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 625811 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 625813 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 625931 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 625932 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 625934 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 625935 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 625936 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 625938 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 626088 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 626090 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 626092 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 626093 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 626094 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 626097 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 626206 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 626208 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 626210 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 626211 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 626212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 626213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 626220 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 626221 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 626222 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 626224 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 626225 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 626226 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 626234 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 626236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 626237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 626238 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0'' 626239 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 626240 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 626348 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0'' 626350 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 626351 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 626456 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 626474 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 627269 DEBUG Test worker d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 627270 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 628907 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 629702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 629702 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 629702 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 629711 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 629719 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 629722 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 629724 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 629726 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 629732 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 629732 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 629737 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 629737 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 629740 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 629750 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 629751 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 629753 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 629805 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 629806 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 629807 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 629808 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 629808 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 629869 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 629870 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 629871 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 629872 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 629872 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 629876 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 629877 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 629877 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 629878 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 629879 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 629880 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 629966 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 629966 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 629967 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 629968 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 629969 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 629970 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 630043 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 630044 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 630045 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 630045 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 630046 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 630047 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 630048 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 630049 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 630049 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 630050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 630050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 630051 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 630051 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 630052 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 630052 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 630053 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 630054 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 630054 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 630055 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 630058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 630090 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 630091 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 630134 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 630135 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 630136 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 630137 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 630138 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 630139 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 630207 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 630212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 630213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 630214 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 630215 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 630216 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 630217 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 630262 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 630265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 630268 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 630321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 630376 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof 631134 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 632772 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 633616 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.64ms 633617 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof