TestContextStatementBlock

1

tests

0

failures

0

ignored

6.409s

duration

100%

successful

Tests

Test Duration Result
testContextTermInstantiation() 6.409s passed

Standard error

700        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: C:\Users\runneradmin\.key\proof-settings.props (The system cannot find the path specified)
	at java.base/java.io.FileInputStream.open0(Native Method)

3816       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
3910       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
3941       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
3956       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Annotation, formerNode: Annotation 
3988       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArithmeticException, formerNode: ArithmeticException 
4019       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayIndexOutOfBoundsException, formerNode: ArrayIndexOutOfBoundsException 
4050       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayStoreException, formerNode: ArrayStoreException 
4081       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: AssertionError, formerNode: AssertionError 
4097       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Character, formerNode: Character 
4113       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
4113       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
4113       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ClassCastException, formerNode: ClassCastException 
4128       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: CloneNotSupportedException, formerNode: CloneNotSupportedException 
4144       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cloneable, formerNode: Cloneable 
4160       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Comparable, formerNode: Comparable 
4175       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Double, formerNode: Double 
4191       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
4191       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
4222       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Error, formerNode: Error 
4238       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Exception, formerNode: Exception 
4285       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
4285       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
4300       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Float, formerNode: Float 
4316       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IllegalArgumentException, formerNode: IllegalArgumentException 
4316       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IndexOutOfBoundsException, formerNode: IndexOutOfBoundsException 
4425       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
4441       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
4441       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InterruptedException, formerNode: InterruptedException 
4441       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterable, formerNode: Iterable 
4457       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkageError, formerNode: LinkageError 
4535       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Math, formerNode: Math 
4535       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NegativeArraySizeException, formerNode: NegativeArraySizeException 
4550       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
4550       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
4550       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NullPointerException, formerNode: NullPointerException 
4550       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Number, formerNode: Number 
4566       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NumberFormatException, formerNode: NumberFormatException 
4582       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: VirtualMachineError, formerNode: VirtualMachineError 
4582       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutOfMemoryError, formerNode: OutOfMemoryError 
4582       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Runnable, formerNode: Runnable 
4597       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: RuntimeException, formerNode: RuntimeException 
4597       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
4649       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
4649       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
4774       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
4805       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
4868       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
4883       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: char, formerNode: /*@ helper */
char 
4883       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: StringBuffer, formerNode: StringBuffer 
4899       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: System, formerNode: System 
4899       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Thread, formerNode: Thread 
4915       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
4915       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
4946       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Collection, formerNode: Collection 
4946       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
4946       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
4961       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
4961       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
5008       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
5008       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
5008       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Long, formerNode: Long 
5008       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Boolean, formerNode: Boolean 
5024       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Map, formerNode: Map 
5055       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
5055       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: FilterOutputStream, formerNode: FilterOutputStream 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IOException, formerNode: IOException 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
5071       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
5102       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
5102       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
5102       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Serializable, formerNode: Serializable 
5102       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
5118       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
5118       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayList, formerNode: ArrayList 
5133       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
5180       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Arrays, formerNode: Arrays 
5180       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIteratorImpl, formerNode: ListIteratorImpl 
5180       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Date, formerNode: Date 
5180       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedHashMap, formerNode: LinkedHashMap 
5196       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: /*@strictly_pure*/
java.lang.String 
5196       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedList, formerNode: LinkedList 
5352       INFO  Test worker     d.u.i.k.n.KeyIO           Parsing took 47 ms 
5352       DEBUG Test worker     d.u.i.k.n.KeyIO           Load declarations of de.uka.ilkd.key.nparser.KeyAst$File:  D:\a\key\key\key.core\src\test\resources\testcase\testrules.key:9#1 
5368       INFO  Test worker     d.u.i.k.n.KeyIO           MODE: declarations took 16 ms 
5368       DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: 2nd degree decls took 0 
5665       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: --#v;, formerNode: --#v 
5696       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: #v = #e;, formerNode: #v = #e 
5712       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: #t, formerNode: #t 
5727       DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: taclets took 359ms