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.048s | passed |
| powPositiveConcrete | data()[101] | 3.033s | passed |
| powGeq1Concrete | data()[102] | 3.051s | passed |
| pow2InIntLower | data()[103] | 3.036s | passed |
| pow2InIntUpper | data()[104] | 3.039s | passed |
| logSelfConcrete | data()[105] | 3.039s | passed |
| log1Concrete | data()[106] | 3.031s | passed |
| logProduct | data()[107] | 3.031s | passed |
| logTimesBaseConcrete | data()[108] | 3.035s | passed |
| logProdIdentity | data()[109] | 3.048s | passed |
| moduloByteIsInByte | data()[10] | 3.117s | passed |
| logProdIdentityConcrete | data()[110] | 3.035s | passed |
| logPowIdentity | data()[111] | 3.034s | passed |
| logPowIdentityConcrete | data()[112] | 3.040s | passed |
| logPositive | data()[113] | 3.037s | passed |
| logPositiveConcrete | data()[114] | 3.034s | passed |
| logMono | data()[115] | 3.042s | passed |
| logMonoConcrete | data()[116] | 3.037s | passed |
| powLogLess | data()[117] | 3.050s | passed |
| powLogMore2 | data()[118] | 3.077s | passed |
| logLessThanPow | data()[119] | 3.052s | passed |
| moduloCharIsInChar | data()[11] | 3.113s | passed |
| logLessThanPowConcrete | data()[120] | 3.060s | passed |
| logSqueeze | data()[121] | 3.047s | passed |
| ifthenelse_equals | data()[122] | 3.047s | passed |
| ifthenelse_equals_1 | data()[123] | 3.059s | passed |
| ifthenelse_equals_2 | data()[124] | 3.046s | passed |
| disjointWithSingleton1 | data()[125] | 3.092s | passed |
| disjointWithSingleton2 | data()[126] | 3.046s | passed |
| disjointArrayRanges | data()[127] | 3.046s | passed |
| disjointArrayRangeAllFields1 | data()[128] | 3.046s | passed |
| disjointArrayRangeAllFields2 | data()[129] | 3.053s | passed |
| div_unique1 | data()[12] | 3.165s | passed |
| seqSelfDefinition | data()[130] | 3.063s | passed |
| seqOutsideValue | data()[131] | 3.049s | passed |
| castedGetAny | data()[132] | 3.047s | passed |
| seqGetAlphaCast | data()[133] | 3.049s | passed |
| getOfSeqSingleton | data()[134] | 3.081s | passed |
| getOfSeqSingletonConcrete | data()[135] | 3.040s | passed |
| getOfSeqConcat | data()[136] | 3.063s | passed |
| getOfSeqSub | data()[137] | 3.047s | passed |
| getOfSeqReverse | data()[138] | 3.053s | passed |
| lenOfSeqEmpty | data()[139] | 3.043s | passed |
| div_unique2 | data()[13] | 3.168s | passed |
| lenOfSeqSingleton | data()[140] | 3.041s | passed |
| lenOfSeqConcat | data()[141] | 3.064s | passed |
| lenOfSeqSub | data()[142] | 3.053s | passed |
| lenOfSeqReverse | data()[143] | 3.056s | passed |
| equalityToSeqGetAndSeqLenLeft | data()[144] | 3.052s | passed |
| equalityToSeqGetAndSeqLenRight | data()[145] | 3.056s | passed |
| getOfSeqSingletonEQ | data()[146] | 3.084s | passed |
| getOfSeqConcatEQ | data()[147] | 3.063s | passed |
| getOfSeqSubEQ | data()[148] | 3.051s | passed |
| getOfSeqReverseEQ | data()[149] | 3.062s | passed |
| div_exists | data()[14] | 3.191s | passed |
| lenOfSeqEmptyEQ | data()[150] | 3.083s | passed |
| lenOfSeqSingletonEQ | data()[151] | 3.057s | passed |
| lenOfSeqConcatEQ | data()[152] | 3.063s | passed |
| lenOfSeqSubEQ | data()[153] | 3.059s | passed |
| lenOfSeqReverseEQ | data()[154] | 3.082s | passed |
| getOfSeqDefEQ | data()[155] | 3.055s | passed |
| lenOfSeqDefEQ | data()[156] | 3.058s | passed |
| seqConcatWithSeqEmpty1 | data()[157] | 3.078s | passed |
| seqConcatWithSeqEmpty2 | data()[158] | 3.044s | passed |
| seqReverseOfSeqEmpty | data()[159] | 3.050s | passed |
| div_one | data()[15] | 3.080s | passed |
| subSeqComplete | data()[160] | 3.066s | passed |
| subSeqTailR | data()[161] | 3.050s | passed |
| subSeqTailL | data()[162] | 3.045s | passed |
| subSeqTailEQR | data()[163] | 3.063s | passed |
| subSeqTailEQL | data()[164] | 3.046s | passed |
| seqDef_split | data()[165] | 3.081s | passed |
| seqDef_induction_upper | data()[166] | 3.061s | passed |
| seqDef_induction_upper_concrete | data()[167] | 3.057s | passed |
| seqDef_induction_lower | data()[168] | 3.085s | passed |
| seqDef_induction_lower_concrete | data()[169] | 3.062s | passed |
| jdiv_one | data()[16] | 3.095s | passed |
| seqDef_split_in_three | data()[170] | 3.099s | passed |
| seqDef_empty | data()[171] | 3.039s | passed |
| seqDef_one_summand | data()[172] | 3.058s | passed |
| seqDef_lower_equals_upper | data()[173] | 3.043s | passed |
| seqDefOfSeq | data()[174] | 3.074s | passed |
| seqSelfDefinitionEQ2 | data()[175] | 3.051s | passed |
| indexOfSeqSingleton | data()[176] | 3.066s | passed |
| indexOfSeqConcatFirst | data()[177] | 3.046s | passed |
| indexOfSeqConcatSecond | data()[178] | 3.064s | passed |
| indexOfSeqSub | data()[179] | 3.044s | passed |
| div_zero | data()[17] | 3.160s | passed |
| lenOfArray2seq | data()[180] | 3.058s | passed |
| getAnyOfArray2seq | data()[181] | 3.034s | passed |
| getOfArray2seq | data()[182] | 3.061s | passed |
| getAnyOfNPermInv | data()[183] | 3.057s | passed |
| seqNPermRange | data()[184] | 3.078s | passed |
| seqPermTrans | data()[185] | 3.096s | passed |
| seqPermRefl | data()[186] | 3.085s | passed |
| seqPermSplit | data()[187] | 3.043s | passed |
| seqNPermRight | data()[188] | 3.129s | passed |
| seqPermFromSwap | data()[189] | 3.103s | passed |
| divResZero1 | data()[18] | 3.125s | passed |
| seqPermTransAlt0 | data()[190] | 3.044s | passed |
| seqPermTransAlt1 | data()[191] | 3.061s | passed |
| seqPermTransAlt2 | data()[192] | 3.057s | passed |
| seqPermTransAlt3 | data()[193] | 3.046s | passed |
| seqPermForall | data()[194] | 3.129s | passed |
| seqPermExists | data()[195] | 3.132s | passed |
| schiffl_lemma_2 | data()[196] | 4.126s | failed |
| schiffl_thm_1 | data()[197] | 3.994s | passed |
| eqSameSeq | data()[198] | 3.174s | passed |
| divResZero2 | data()[19] | 3.086s | passed |
| eqTermCut | data()[1] | 3.656s | passed |
| divResOne1 | data()[20] | 3.075s | passed |
| divResOne2 | data()[21] | 3.113s | passed |
| div_cancel1 | data()[22] | 3.098s | passed |
| div_cancel2 | data()[23] | 3.088s | passed |
| divAddMultDenom | data()[24] | 3.093s | passed |
| divMinus | data()[25] | 3.155s | passed |
| divMinusDenom | data()[26] | 3.098s | passed |
| divLeastDPos | data()[27] | 3.075s | passed |
| divLeastDNeg | data()[28] | 3.073s | passed |
| divGreatestDPos | data()[29] | 3.061s | passed |
| equivAllRight | data()[2] | 3.316s | passed |
| divGreatestDNeg | data()[30] | 3.053s | passed |
| divIncreasingPos | data()[31] | 3.074s | passed |
| divIncreasingNeg | data()[32] | 3.101s | passed |
| jdiv_zero | data()[33] | 3.061s | passed |
| jdivPulloutMinusNum | data()[34] | 3.056s | passed |
| jdivPulloutMinusDenom | data()[35] | 3.124s | passed |
| jdiv_uniquePosPos | data()[36] | 3.062s | passed |
| jdiv_uniquePosNeg | data()[37] | 3.060s | passed |
| jdiv_uniqueNegPos | data()[38] | 3.078s | passed |
| jdiv_uniqueNegNeg | data()[39] | 3.072s | passed |
| irrflConcrete1 | data()[3] | 3.375s | passed |
| jdivMultDenom1 | data()[40] | 3.069s | passed |
| jdivMultDenom2 | data()[41] | 3.050s | passed |
| mod_geZero | data()[42] | 3.058s | passed |
| mod_lessDenom | data()[43] | 3.097s | passed |
| jmod_NumPos | data()[44] | 3.047s | passed |
| jmod_NumNeg | data()[45] | 3.059s | passed |
| jmod_geZero | data()[46] | 3.065s | passed |
| jmodNumZero | data()[47] | 3.049s | passed |
| jmod_pulloutminusNum | data()[48] | 3.054s | passed |
| jmod_pulloutminusDenom | data()[49] | 3.064s | passed |
| irrflConcrete2 | data()[4] | 3.272s | passed |
| jmodUnique1 | data()[50] | 3.094s | passed |
| jmodUnique2 | data()[51] | 3.129s | passed |
| intDivRem | data()[52] | 3.077s | passed |
| jmodjmod | data()[53] | 3.091s | passed |
| jmodDivisible | data()[54] | 3.064s | passed |
| jmodDivisibleRep | data()[55] | 3.051s | passed |
| jdivAddMultDenom | data()[56] | 3.137s | passed |
| jmodAltZero | data()[57] | 3.064s | passed |
| jmodAddMultDenomZero | data()[58] | 3.099s | passed |
| polyDiv_zero | data()[59] | 3.084s | passed |
| cancel_gtPos | data()[5] | 3.203s | passed |
| polyMod_ltdivDenom | data()[60] | 3.040s | passed |
| bsum_empty | data()[61] | 3.032s | passed |
| bsum_induction_upper | data()[62] | 3.029s | passed |
| bsum_induction_lower | data()[63] | 3.053s | passed |
| bsum_num_of_bounds | data()[64] | 3.051s | passed |
| bsum_num_of_bounds2 | data()[65] | 3.064s | passed |
| bsum_induction_upper2 | data()[66] | 3.048s | passed |
| bsum_induction_upper_concrete | data()[67] | 3.043s | passed |
| bsum_induction_upper_concrete_2 | data()[68] | 3.038s | passed |
| bsum_induction_upper2_concrete | data()[69] | 3.040s | passed |
| cancel_gtNeg | data()[6] | 3.219s | passed |
| bsum_induction_lower_concrete | data()[70] | 3.037s | passed |
| bsum_induction_lower2 | data()[71] | 3.031s | passed |
| bsum_induction_lower2_concrete | data()[72] | 3.039s | passed |
| bsum_positive | data()[73] | 3.067s | passed |
| bsum_upper_bound | data()[74] | 3.071s | passed |
| bsum_lower_bound | data()[75] | 3.072s | passed |
| bsum_positive_lower_bound_element | data()[76] | 3.092s | passed |
| bsum_sub_same_index | data()[77] | 3.061s | passed |
| bsum_less_same_index | data()[78] | 3.079s | passed |
| bsum_equal_except_one_index | data()[79] | 3.074s | passed |
| moduloIntIsInInt | data()[7] | 3.138s | passed |
| bsum_num_of_is_max | data()[80] | 3.054s | passed |
| bsum_num_of_is_max2 | data()[81] | 3.049s | passed |
| bsum_num_of_is_max3 | data()[82] | 3.044s | passed |
| bsum_num_of_is_max4 | data()[83] | 3.057s | passed |
| bsum_num_of_lt_max | data()[84] | 3.060s | passed |
| bsum_num_of_lt_max2 | data()[85] | 3.065s | passed |
| bsum_num_of_lt_max3 | data()[86] | 3.071s | passed |
| bsum_num_of_lt_max4 | data()[87] | 3.106s | passed |
| bsum_num_of_gt0 | data()[88] | 3.087s | passed |
| bsum_num_of_gt0_alt | data()[89] | 3.060s | passed |
| moduloLongIsInLong | data()[8] | 3.173s | passed |
| bsum_add_concrete | data()[90] | 3.070s | passed |
| bprod_all_positive | data()[91] | 3.063s | passed |
| bprod_split | data()[92] | 3.055s | passed |
| powConcrete0 | data()[93] | 3.037s | passed |
| powConcrete1 | data()[94] | 3.042s | passed |
| powSplitFactor | data()[95] | 3.046s | passed |
| powAdd | data()[96] | 3.043s | passed |
| powMono | data()[97] | 3.052s | passed |
| powMonoConcrete | data()[98] | 3.038s | passed |
| powMonoConcreteRight | data()[99] | 3.045s | passed |
| moduloShortIsInShort | data()[9] | 3.139s | passed |
Standard output
318 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file src/test/resources/testcase/dummyTrue.key 594 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) 599 DEBUG Test worker d.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 628 DEBUG Test worker d.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 634 DEBUG Test worker d.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 647 DEBUG Test worker d.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 694 DEBUG Test worker d.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 704 DEBUG Test worker d.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 710 DEBUG Test worker d.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 716 DEBUG Test worker d.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 719 DEBUG Test worker d.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 721 DEBUG Test worker d.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 722 DEBUG Test worker d.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 724 DEBUG Test worker d.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 774 DEBUG Test worker d.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 778 DEBUG Test worker d.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 781 DEBUG Test worker d.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 929 DEBUG Test worker d.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 979 DEBUG Test worker d.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 1021 DEBUG Test worker d.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 1060 DEBUG Test worker d.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 1182 DEBUG Test worker d.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 1217 DEBUG Test worker d.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 1328 DEBUG Test worker d.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 1364 DEBUG Test worker d.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 1373 DEBUG Test worker d.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 1377 DEBUG Test worker d.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 1387 DEBUG Test worker d.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 1519 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1519 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1520 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1520 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta 1542 DEBUG Test worker d.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 1567 DEBUG Test worker d.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 1673 DEBUG Test worker d.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 1721 DEBUG Test worker d.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 1724 DEBUG Test worker d.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 1731 DEBUG Test worker d.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 1747 DEBUG Test worker d.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 1769 DEBUG Test worker d.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 1770 DEBUG Test worker d.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 1770 DEBUG Test worker d.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 1809 DEBUG Test worker d.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 1834 DEBUG Test worker d.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 1840 DEBUG Test worker d.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 1847 DEBUG Test worker d.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 1916 DEBUG Test worker d.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 1983 DEBUG Test worker d.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 2011 DEBUG Test worker d.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 2070 DEBUG Test worker d.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 2074 DEBUG Test worker d.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 2167 DEBUG Test worker d.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 2213 DEBUG Test worker d.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 2224 DEBUG Test worker d.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 2394 DEBUG Test worker d.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 2928 DEBUG Test worker d.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 2941 DEBUG Test worker d.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 2992 DEBUG Test worker d.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 3011 DEBUG Test worker d.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 3015 DEBUG Test worker d.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 3077 DEBUG Test worker d.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 3098 DEBUG Test worker d.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 3119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression 3121 DEBUG Test worker d.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 3138 DEBUG Test worker d.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 3142 DEBUG Test worker d.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 3156 DEBUG Test worker d.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 3158 DEBUG Test worker d.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 3159 DEBUG Test worker d.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 3163 DEBUG Test worker d.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 3168 DEBUG Test worker d.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 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/infFlow.key 3181 DEBUG Test worker d.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 3186 DEBUG Test worker d.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 3187 DEBUG Test worker d.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 3190 DEBUG Test worker d.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 3194 DEBUG Test worker d.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 3216 DEBUG Test worker d.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 3221 DEBUG Test worker d.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 3225 DEBUG Test worker d.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 3227 DEBUG Test worker d.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 3230 DEBUG Test worker d.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 3233 DEBUG Test worker d.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 3235 DEBUG Test worker d.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 3278 DEBUG Test worker d.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 3282 DEBUG Test worker d.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 3284 DEBUG Test worker d.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 3360 DEBUG Test worker d.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 6107 DEBUG Test worker d.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 8270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ns 8271 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file src/test/resources/testcase/dummyTrue.key 8283 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 9254 DEBUG Test worker d.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 10978 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 11932 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 11932 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 11941 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 12746 DEBUG Test worker d.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 14451 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 15254 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 15255 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 15258 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 16140 DEBUG Test worker d.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 17852 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 18631 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 18631 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 18634 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 19421 DEBUG Test worker d.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 21091 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 21902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 21903 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 21908 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 22649 DEBUG Test worker d.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 24288 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 25105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.36ms 25106 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 25110 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 25907 DEBUG Test worker d.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 27532 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 28321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 28322 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 28329 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 29059 DEBUG Test worker d.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 30689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 31464 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.21ns 31465 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 31467 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 32196 DEBUG Test worker d.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 33841 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 34637 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.61ns 34638 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 34640 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 35370 DEBUG Test worker d.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 37002 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 37776 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.21ns 37777 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 37779 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 38506 DEBUG Test worker d.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 40125 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 40894 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.71ns 40894 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 40896 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 41628 DEBUG Test worker d.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 43229 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 44006 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.71ns 44007 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 44009 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 44741 DEBUG Test worker d.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 46364 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 47173 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.81ms 47173 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 47177 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 47941 DEBUG Test worker d.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 49517 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 50341 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.19ms 50342 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 50345 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 51104 DEBUG Test worker d.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 52665 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 53533 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.77ms 53533 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 53536 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 54284 DEBUG Test worker d.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 55846 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 56614 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 56615 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 56616 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 57365 DEBUG Test worker d.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 58926 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 59709 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 59709 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 59712 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 60459 DEBUG Test worker d.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 62023 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 62870 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.9ms 62870 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 62874 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 63622 DEBUG Test worker d.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 65196 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 65996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 65996 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 65998 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 66744 DEBUG Test worker d.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 68306 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 69082 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms 69082 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 69084 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 69829 DEBUG Test worker d.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 71388 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 72157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 72158 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 72159 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 72904 DEBUG Test worker d.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 74464 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 75270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 75270 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 75272 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 76028 DEBUG Test worker d.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 77591 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 78368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 78368 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 78370 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 79118 DEBUG Test worker d.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 80719 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 81456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 81456 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 81458 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 82205 DEBUG Test worker d.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 83785 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 84549 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.59ms 84549 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 84551 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 85291 DEBUG Test worker d.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 86894 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 87698 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.87ms 87699 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 87706 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 88464 DEBUG Test worker d.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 90042 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 90803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.15ms 90804 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 90805 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 91565 DEBUG Test worker d.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 93140 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 93878 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 93879 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 93880 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 94624 DEBUG Test worker d.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 96208 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 96951 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 96951 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 96952 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 97693 DEBUG Test worker d.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 99272 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 100012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.13ms 100012 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 100014 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 100755 DEBUG Test worker d.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 102326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 103065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 103065 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 103066 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 103811 DEBUG Test worker d.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 105397 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 106139 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 106140 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 106142 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 106893 DEBUG Test worker d.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 108467 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 109241 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 109241 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 109242 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 109959 DEBUG Test worker d.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 111537 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 112301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 112301 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 112302 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 113017 DEBUG Test worker d.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 114594 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 115357 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 115357 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 115369 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 116113 DEBUG Test worker d.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 117696 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 118481 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.11ms 118481 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 118484 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 119200 DEBUG Test worker d.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 120779 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 121543 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 121543 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 121544 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 122259 DEBUG Test worker d.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 123835 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 124603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 124603 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 124604 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 125319 DEBUG Test worker d.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 126913 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 127681 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 127681 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 127682 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 128397 DEBUG Test worker d.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 129985 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 130752 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 130753 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 130755 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 131471 DEBUG Test worker d.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 133042 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 133822 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.07ms 133822 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 133824 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 134563 DEBUG Test worker d.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 136111 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 136873 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.52ns 136873 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 136874 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 137611 DEBUG Test worker d.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 139163 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 139930 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 139931 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 139932 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 140702 DEBUG Test worker d.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 142263 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 143027 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 143027 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 143029 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 143765 DEBUG Test worker d.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 145311 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 146074 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 146075 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 146076 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 146813 DEBUG Test worker d.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 148363 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 149133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 149133 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 149134 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 149872 DEBUG Test worker d.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 151433 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 152198 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 152198 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 152199 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 152938 DEBUG Test worker d.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 154488 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 155246 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 155247 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 155249 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 155989 DEBUG Test worker d.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 157542 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 158301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 158301 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 158303 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 159042 DEBUG Test worker d.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 160607 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 161364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 161365 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 161367 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 162104 DEBUG Test worker d.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 163653 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 164459 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.33ms 164460 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 164461 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 165200 DEBUG Test worker d.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 166767 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 167587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.79ms 167587 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 167590 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 168330 DEBUG Test worker d.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 169915 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 170661 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 170665 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 170666 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 171424 DEBUG Test worker d.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 172999 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 173757 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.73ms 173757 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 173758 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 174496 DEBUG Test worker d.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 176067 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 176821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.53ms 176821 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 176822 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 177567 DEBUG Test worker d.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 179140 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 179872 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 179872 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 179873 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 180608 DEBUG Test worker d.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 182177 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 183007 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.66ms 183007 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 183010 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 183754 DEBUG Test worker d.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 185330 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 186072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 186072 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 186074 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 186833 DEBUG Test worker d.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 188435 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 189171 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 189172 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 189173 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 189909 DEBUG Test worker d.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 191484 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 192256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 192256 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 192257 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 192969 DEBUG Test worker d.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 194535 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 195294 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 195295 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 195297 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 196009 DEBUG Test worker d.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 197577 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 198327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 198327 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 198328 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 199039 DEBUG Test worker d.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 200603 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 201356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 201357 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 201358 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 202072 DEBUG Test worker d.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 203644 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 204409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.36ms 204409 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 204411 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 205125 DEBUG Test worker d.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 206696 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 207460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 207460 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 207462 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 208178 DEBUG Test worker d.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 209760 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 210524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 210524 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 210525 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 211239 DEBUG Test worker d.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 212819 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 213573 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.73ns 213573 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 213574 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 214286 DEBUG Test worker d.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 215861 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 216615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 216615 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 216617 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 217328 DEBUG Test worker d.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 218897 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 219653 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 219653 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 219655 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 220395 DEBUG Test worker d.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 221940 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 222694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 864.52ns 222694 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 222695 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 223431 DEBUG Test worker d.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 224976 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 225731 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.21ns 225731 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 225732 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 226467 DEBUG Test worker d.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 228007 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 228761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 228762 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 228763 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 229498 DEBUG Test worker d.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 231047 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 231800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.12ns 231800 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 231801 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 232539 DEBUG Test worker d.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 234084 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 234867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.64ms 234868 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 234869 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 235607 DEBUG Test worker d.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 237155 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 237939 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.71ms 237939 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 237940 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 238677 DEBUG Test worker d.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 240230 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 241010 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.86ms 241011 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 241013 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 241755 DEBUG Test worker d.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 243311 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 244102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.34ms 244103 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 244104 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 244842 DEBUG Test worker d.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 246391 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 247164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.51ms 247164 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 247165 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 247905 DEBUG Test worker d.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 249450 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 250242 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.18ms 250242 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 250244 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 251004 DEBUG Test worker d.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 252548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 253317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms 253317 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 253318 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 254053 DEBUG Test worker d.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 255627 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 256370 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.58ms 256371 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 256372 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 257110 DEBUG Test worker d.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 258676 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 259419 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.35ms 259419 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 259421 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 260157 DEBUG Test worker d.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 261722 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 262463 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 262463 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 262464 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 263208 DEBUG Test worker d.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 264774 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 265520 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 265520 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 265521 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 266264 DEBUG Test worker d.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 267834 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 268581 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ms 268581 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 268582 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 269317 DEBUG Test worker d.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 270897 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 271645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 271645 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 271646 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 272390 DEBUG Test worker d.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 273964 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 274716 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.25ms 274716 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 274718 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 275506 DEBUG Test worker d.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 277076 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 277822 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 277822 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 277824 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 278564 DEBUG Test worker d.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 280142 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 280910 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 280910 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 280911 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 281625 DEBUG Test worker d.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 283202 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 283969 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.81ms 283969 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 283971 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 284686 DEBUG Test worker d.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 286259 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 287039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 287040 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 287041 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 287758 DEBUG Test worker d.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 289333 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 290102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 290102 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 290104 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 290818 DEBUG Test worker d.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 292403 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 293158 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 293158 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 293159 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 293870 DEBUG Test worker d.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 295440 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 296194 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.61ns 296195 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 296196 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 296908 DEBUG Test worker d.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 298483 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 299236 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.41ns 299236 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 299237 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 299949 DEBUG Test worker d.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 301522 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 302282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 302282 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 302284 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 302997 DEBUG Test worker d.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 304566 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 305325 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 305326 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 305327 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 306061 DEBUG Test worker d.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 307611 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 308377 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 308377 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 308378 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 309114 DEBUG Test worker d.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 310656 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 311415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 311415 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 311417 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 312154 DEBUG Test worker d.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 313706 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 314460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 477.81ns 314461 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 314462 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 315205 DEBUG Test worker d.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 316747 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 317509 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 317509 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 317510 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 318246 DEBUG Test worker d.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 319786 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 320541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 586.81ns 320541 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 320542 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 321281 DEBUG Test worker d.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 322830 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 323592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 472.91ns 323592 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 323593 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 324328 DEBUG Test worker d.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 325873 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 326629 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.91ns 326629 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 326630 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 327368 DEBUG Test worker d.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 328910 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 329668 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 329668 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 329669 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 330406 DEBUG Test worker d.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 331946 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 332706 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 332707 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 332708 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 333441 DEBUG Test worker d.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 334983 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 335737 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 335737 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 335738 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 336471 DEBUG Test worker d.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 338011 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 338768 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 338768 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 338769 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 339504 DEBUG Test worker d.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 341047 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 341803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 341803 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 341805 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 342539 DEBUG Test worker d.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 344106 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 344851 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 344851 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 344852 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 345588 DEBUG Test worker d.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 347155 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 347886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 347886 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 347887 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 348621 DEBUG Test worker d.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 350189 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 350920 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.32ns 350920 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 350921 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 351653 DEBUG Test worker d.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 353228 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 353961 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 353961 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 353962 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 354695 DEBUG Test worker d.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 356258 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 356997 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 356998 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 356999 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 357732 DEBUG Test worker d.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 359298 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 360030 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.61ns 360031 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 360032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 360767 DEBUG Test worker d.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 362321 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 363073 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.62ms 363074 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 363075 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 363816 DEBUG Test worker d.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 365381 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 366111 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 366111 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 366112 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 366845 DEBUG Test worker d.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 368417 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 369160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 369160 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 369161 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 369898 DEBUG Test worker d.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 371467 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 372237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.83ms 372238 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 372239 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 372951 DEBUG Test worker d.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 374521 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 375289 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 375290 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 375291 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 376004 DEBUG Test worker d.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 377594 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 378350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.71ns 378350 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 378351 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 379063 DEBUG Test worker d.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 380636 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 381396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 381396 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 381397 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 382110 DEBUG Test worker d.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 383685 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 384443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 384443 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 384445 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 385156 DEBUG Test worker d.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 386744 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 387502 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.42ns 387502 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 387503 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 388213 DEBUG Test worker d.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 389786 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 390549 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.52ns 390549 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 390550 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 391263 DEBUG Test worker d.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 392874 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 393640 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 393641 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 393643 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 394357 DEBUG Test worker d.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 395928 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 396687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 396687 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 396688 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 397424 DEBUG Test worker d.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 398967 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 399733 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 399733 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 399734 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 400469 DEBUG Test worker d.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 402014 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 402778 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 402778 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 402779 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 403513 DEBUG Test worker d.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 405056 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 405831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 405831 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 405833 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 406569 DEBUG Test worker d.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 408115 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 408894 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 408894 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 408896 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 409634 DEBUG Test worker d.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 411173 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 411943 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 411944 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 411945 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 412680 DEBUG Test worker d.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 414243 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 414991 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 414991 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 414992 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 415732 DEBUG Test worker d.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 417296 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 418040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830.52ns 418040 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 418041 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 418773 DEBUG Test worker d.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 420336 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 421119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.12ns 421120 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 421122 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 421832 DEBUG Test worker d.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 423395 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 424160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.02ns 424161 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 424162 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 424872 DEBUG Test worker d.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 426440 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 427224 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 427224 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 427225 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 427937 DEBUG Test worker d.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 429502 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 430270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 430270 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 430271 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 431006 DEBUG Test worker d.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 432546 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 433323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 433324 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 433325 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 434060 DEBUG Test worker d.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 435600 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 436366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.91ns 436366 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 436367 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 437103 DEBUG Test worker d.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 438664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 439407 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.11ns 439407 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 439408 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 440143 DEBUG Test worker d.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 441704 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 442471 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 442471 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 442472 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 443186 DEBUG Test worker d.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 444756 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 445525 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.01ns 445525 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 445526 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 446237 DEBUG Test worker d.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 447811 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 448580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.32ns 448580 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 448581 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 449318 DEBUG Test worker d.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 450865 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 451633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 451633 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 451634 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 452369 DEBUG Test worker d.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 453941 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 454689 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 454689 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 454690 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 455426 DEBUG Test worker d.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 457002 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 457772 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 902.32ns 457773 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 457774 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 458487 DEBUG Test worker d.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 460060 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 460835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 460835 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 460836 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 461573 DEBUG Test worker d.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 463120 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 463887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 631.51ns 463887 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 463888 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 464625 DEBUG Test worker d.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 466175 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 466948 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 466948 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 466949 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 467683 DEBUG Test worker d.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 469256 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 470031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.12ns 470031 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 470032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 470745 DEBUG Test worker d.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 472319 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 473088 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.92ns 473088 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 473090 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 473822 DEBUG Test worker d.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 475379 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 476151 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 476151 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 476152 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 476890 DEBUG Test worker d.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 478464 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 479210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.62ns 479211 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 479212 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 479951 DEBUG Test worker d.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 481523 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 482292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 482292 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 482293 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 483004 DEBUG Test worker d.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 484578 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 485347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 485348 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 485350 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 486084 DEBUG Test worker d.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 487632 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 488405 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 488405 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 488406 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 489141 DEBUG Test worker d.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 490710 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 491483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 491483 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 491484 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 492194 DEBUG Test worker d.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 493758 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 494527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 494527 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 494528 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 495266 DEBUG Test worker d.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 496808 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 497577 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 497578 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 497579 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 498312 DEBUG Test worker d.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 499875 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 500644 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 500644 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 500645 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 501355 DEBUG Test worker d.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 502921 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 503693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 503694 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 503695 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 504425 DEBUG Test worker d.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 505988 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 506738 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 506738 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 506740 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 507472 DEBUG Test worker d.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 509030 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 509801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 509801 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 509802 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 510512 DEBUG Test worker d.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 512077 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 512847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 512847 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 512849 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 513583 DEBUG Test worker d.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 515145 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 515928 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.58ms 515928 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 515930 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 516641 DEBUG Test worker d.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 518207 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 518989 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.65ms 518989 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 518991 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 519726 DEBUG Test worker d.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 521287 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 522046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 522046 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 522047 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 522793 DEBUG Test worker d.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 524354 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 525131 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 525131 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 525133 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 525863 DEBUG Test worker d.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 527409 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 528193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 528193 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 528194 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 528927 DEBUG Test worker d.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 530487 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 531292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.01ms 531292 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 531294 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 532024 DEBUG Test worker d.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 533565 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 534332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 534332 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 534333 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 535064 DEBUG Test worker d.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 536624 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 537389 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 537389 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 537390 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 538126 DEBUG Test worker d.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 539664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 540432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 540433 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 540434 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 541167 DEBUG Test worker d.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 542729 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 543506 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 543507 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 543508 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 544220 DEBUG Test worker d.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 545787 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 546557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 546557 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 546558 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 547291 DEBUG Test worker d.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 548857 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 549623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 549623 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 549625 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 550357 DEBUG Test worker d.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 551896 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 552670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 552670 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 552671 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 553404 DEBUG Test worker d.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 554962 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 555734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 555734 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 555735 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 556465 DEBUG Test worker d.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 558004 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 558777 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ms 558777 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 558778 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 559513 DEBUG Test worker d.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 561071 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 561835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 947.62ns 561835 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 561836 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 562565 DEBUG Test worker d.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 564124 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 564870 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 564870 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 564871 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 565603 DEBUG Test worker d.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 567163 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 567931 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 567931 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 567932 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 568661 DEBUG Test worker d.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 570223 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 570988 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 570988 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 570989 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 571700 DEBUG Test worker d.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 573262 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 574065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.47ms 574065 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 574067 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 574804 DEBUG Test worker d.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 576385 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 577162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 577162 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 577163 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 577894 DEBUG Test worker d.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 579461 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 580247 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.09ms 580247 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 580248 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 580961 DEBUG Test worker d.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 582522 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 583290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.2ns 583290 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 583291 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 584026 DEBUG Test worker d.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 585583 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 586418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.71ms 586418 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 586420 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 587152 DEBUG Test worker d.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 588719 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 589521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.27ms 589521 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 589522 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 590234 DEBUG Test worker d.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 591801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 592566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.3ns 592566 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 592568 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 593302 DEBUG Test worker d.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 594862 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 595627 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 210.8ns 595627 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 595628 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 596364 DEBUG Test worker d.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 597921 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 598684 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.1ns 598684 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 598686 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 599398 DEBUG Test worker d.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 600965 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 601730 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.21ns 601730 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 601731 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 602458 DEBUG Test worker d.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 604014 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 604858 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.77ms 604858 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 604861 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 605601 DEBUG Test worker d.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 607178 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 607990 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.85ms 607990 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 607992 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 608729 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 608730 DEBUG Test worker d.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 610307 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 611080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 611080 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 611105 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 611139 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 611157 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 611162 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 611179 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 611180 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 611182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 611183 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 611189 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange' 611190 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 611196 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 611198 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 611406 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 611407 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 611408 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 611409 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 611410 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 611530 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 611531 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 611535 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 611536 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 611537 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 611539 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 611709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 611710 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 611711 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 611712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 611712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 611713 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 611831 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 611832 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 611833 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 611834 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 611834 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 611835 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 611842 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 611842 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 611843 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 611845 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 611845 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 611846 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 611853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 611853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 611854 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 611855 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0'' 611855 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 611856 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 611989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0'' 611990 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 611991 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 612113 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 612120 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 613026 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 613027 DEBUG Test worker d.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 614625 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 615408 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 615408 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 615409 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 615416 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 615425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 615428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 615431 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 615434 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 615439 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 615440 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 615444 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 615445 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 615448 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 615463 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 615464 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 615466 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 615533 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 615534 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 615534 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 615535 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 615536 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 615594 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 615594 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 615595 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 615596 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 615597 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 615601 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 615601 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 615602 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 615602 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 615603 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 615604 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 615680 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 615681 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 615681 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 615682 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 615683 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 615684 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 615756 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 615757 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 615758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 615758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 615759 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 615760 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 615760 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 615761 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 615761 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 615762 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 615762 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 615762 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 615763 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 615763 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 615764 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 615764 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 615765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 615765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 615766 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 615769 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 615805 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 615806 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 615858 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 615859 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 615860 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 615861 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 615862 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 615863 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 615946 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 615948 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 615949 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 615950 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 615951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 615952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 615952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 615998 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 616000 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 616003 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 616058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 616113 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof 616862 DEBUG Test worker d.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 618453 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 619278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 619279 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof