TestTacletIndex

5

tests

0

failures

1

ignored

0.414s

duration

100%

successful

Tests

Test Duration Result
disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed() - ignored
testMatchConflictOccurs() 0.002s passed
testNoMatchingFindRule() 0.002s passed
testNotFreeInYConflict() 0.009s passed
testShownIfHeuristicFits() 0.400s passed

Standard error

80432      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
80437      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
80438      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
80439      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Annotation, formerNode: Annotation 
80442      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArithmeticException, formerNode: ArithmeticException 
80444      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayIndexOutOfBoundsException, formerNode: ArrayIndexOutOfBoundsException 
80445      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayStoreException, formerNode: ArrayStoreException 
80447      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: AssertionError, formerNode: AssertionError 
80449      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Character, formerNode: Character 
80450      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
80450      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
80451      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ClassCastException, formerNode: ClassCastException 
80453      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: CloneNotSupportedException, formerNode: CloneNotSupportedException 
80453      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cloneable, formerNode: Cloneable 
80454      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Comparable, formerNode: Comparable 
80455      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Double, formerNode: Double 
80457      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
80458      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
80460      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Error, formerNode: Error 
80462      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Exception, formerNode: Exception 
80464      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
80464      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
80466      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Float, formerNode: Float 
80467      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IllegalArgumentException, formerNode: IllegalArgumentException 
80468      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IndexOutOfBoundsException, formerNode: IndexOutOfBoundsException 
80483      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
80483      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
80484      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InterruptedException, formerNode: InterruptedException 
80485      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterable, formerNode: Iterable 
80486      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkageError, formerNode: LinkageError 
80495      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Math, formerNode: Math 
80497      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NegativeArraySizeException, formerNode: NegativeArraySizeException 
80498      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
80498      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
80500      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NullPointerException, formerNode: NullPointerException 
80501      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Number, formerNode: Number 
80503      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NumberFormatException, formerNode: NumberFormatException 
80504      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: VirtualMachineError, formerNode: VirtualMachineError 
80505      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutOfMemoryError, formerNode: OutOfMemoryError 
80506      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Runnable, formerNode: Runnable 
80508      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: RuntimeException, formerNode: RuntimeException 
80508      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
80513      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
80513      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
80524      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
80536      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
80557      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
80559      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: char, formerNode: /*@ helper */
char 
80560      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: StringBuffer, formerNode: StringBuffer 
80563      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: System, formerNode: System 
80564      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Thread, formerNode: Thread 
80567      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
80567      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
80572      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Collection, formerNode: Collection 
80573      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
80573      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
80577      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
80577      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
80579      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
80579      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
80580      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Long, formerNode: Long 
80581      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Boolean, formerNode: Boolean 
80585      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Map, formerNode: Map 
80588      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
80589      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
80590      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: FilterOutputStream, formerNode: FilterOutputStream 
80590      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
80591      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
80592      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IOException, formerNode: IOException 
80593      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
80593      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
80598      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
80598      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
80599      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Serializable, formerNode: Serializable 
80600      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
80602      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
80603      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayList, formerNode: ArrayList 
80605      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
80624      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Arrays, formerNode: Arrays 
80625      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIteratorImpl, formerNode: ListIteratorImpl 
80626      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Date, formerNode: Date 
80627      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedHashMap, formerNode: LinkedHashMap 
80628      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: /*@strictly_pure*/
java.lang.String 
80629      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedList, formerNode: LinkedList 
80642      INFO  Test worker     d.u.i.k.n.KeyIO           Parsing took 1 ms 
80642      DEBUG Test worker     d.u.i.k.n.KeyIO           Load declarations of de.uka.ilkd.key.nparser.KeyAst$File:  /home/runner/work/key/key/key.core/src/test/resources/testcase/../de/uka/ilkd/key/proof/ruleForTestTacletIndex.taclet:7#1 
80646      INFO  Test worker     d.u.i.k.n.KeyIO           MODE: declarations took 4 ms 
80646      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: 2nd degree decls took 0 
80653      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: taclets took 6ms