TestTacletEquality

1

tests

1

failures

0

ignored

0s

duration

0%

successful

Failed tests

initializationError

java.io.IOException: Contract not found: Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0
	at de.uka.ilkd.key.proof.init.FunctionalOperationContractPO.loadFrom(FunctionalOperationContractPO.java:379)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:568)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createProofObligationContainer(AbstractProblemLoader.java:628)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:278)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:257)
	at de.uka.ilkd.key.nparser.TestTacletEquality.setUp(TestTacletEquality.java:99)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:568)
	at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:727)
	at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
	at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
	at org.junit.jupiter.engine.extension.TimeoutExtension.interceptLifecycleMethod(TimeoutExtension.java:128)
	at org.junit.jupiter.engine.extension.TimeoutExtension.interceptBeforeAllMethod(TimeoutExtension.java:70)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
	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.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
	at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
	at org.junit.jupiter.engine.descriptor.ClassBasedTestDescriptor.lambda$invokeBeforeAllMethods$13(ClassBasedTestDescriptor.java:411)
	at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at org.junit.jupiter.engine.descriptor.ClassBasedTestDescriptor.invokeBeforeAllMethods(ClassBasedTestDescriptor.java:409)
	at org.junit.jupiter.engine.descriptor.ClassBasedTestDescriptor.before(ClassBasedTestDescriptor.java:215)
	at org.junit.jupiter.engine.descriptor.ClassBasedTestDescriptor.before(ClassBasedTestDescriptor.java:84)
	at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:148)
	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:1511)
	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:77)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:568)
	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 jdk.proxy2/jdk.proxy2.$Proxy5.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 Duration Result
initializationError 0s failed

Standard error

48835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
48835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.7ns 
48835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49100      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Annotation, formerNode: Annotation 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArithmeticException, formerNode: ArithmeticException 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayIndexOutOfBoundsException, formerNode: ArrayIndexOutOfBoundsException 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayStoreException, formerNode: ArrayStoreException 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: AssertionError, formerNode: AssertionError 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Character, formerNode: Character 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
49116      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ClassCastException, formerNode: ClassCastException 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: CloneNotSupportedException, formerNode: CloneNotSupportedException 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cloneable, formerNode: Cloneable 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Comparable, formerNode: Comparable 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Double, formerNode: Double 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Error, formerNode: Error 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Exception, formerNode: Exception 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
49131      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Float, formerNode: Float 
49147      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IllegalArgumentException, formerNode: IllegalArgumentException 
49147      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IndexOutOfBoundsException, formerNode: IndexOutOfBoundsException 
49163      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
49163      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
49163      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InterruptedException, formerNode: InterruptedException 
49163      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterable, formerNode: Iterable 
49163      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkageError, formerNode: LinkageError 
49178      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Math, formerNode: Math 
49178      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NegativeArraySizeException, formerNode: NegativeArraySizeException 
49178      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
49178      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
49178      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NullPointerException, formerNode: NullPointerException 
49194      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Number, formerNode: Number 
49196      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NumberFormatException, formerNode: NumberFormatException 
49198      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: VirtualMachineError, formerNode: VirtualMachineError 
49201      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutOfMemoryError, formerNode: OutOfMemoryError 
49201      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Runnable, formerNode: Runnable 
49201      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: RuntimeException, formerNode: RuntimeException 
49201      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
49201      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
49217      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
49232      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
49250      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
49279      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
49279      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: char, formerNode: /*@ helper */
char 
49279      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: StringBuffer, formerNode: StringBuffer 
49279      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: System, formerNode: System 
49279      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Thread, formerNode: Thread 
49295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
49295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
49295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Collection, formerNode: Collection 
49295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
49295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Long, formerNode: Long 
49310      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Boolean, formerNode: Boolean 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Map, formerNode: Map 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: FilterOutputStream, formerNode: FilterOutputStream 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IOException, formerNode: IOException 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
49326      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
49342      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
49342      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
49342      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Serializable, formerNode: Serializable 
49342      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
49342      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
49359      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayList, formerNode: ArrayList 
49359      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Arrays, formerNode: Arrays 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIteratorImpl, formerNode: ListIteratorImpl 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Date, formerNode: Date 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedHashMap, formerNode: LinkedHashMap 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: /*@strictly_pure*/
java.lang.String 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedList, formerNode: LinkedList 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: A, formerNode: A 
49391      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Gcd, formerNode: Gcd 
49406      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: a = -a;, formerNode: a = -a 
49406      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: b = -b;, formerNode: b = -b 
49531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 704.82ms