TestTacletIndex

5

tests

0

failures

1

ignored

0.531s

duration

100%

successful

Tests

Test Duration Result
disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed() - ignored
testMatchConflictOccurs() 0.002s passed
testNoMatchingFindRule() 0.002s passed
testNotFreeInYConflict() 0.010s passed
testShownIfHeuristicFits() 0.517s passed

Standard error

91437      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
91443      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
91443      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
91445      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Annotation, formerNode: Annotation 
91448      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArithmeticException, formerNode: ArithmeticException 
91450      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayIndexOutOfBoundsException, formerNode: ArrayIndexOutOfBoundsException 
91452      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayStoreException, formerNode: ArrayStoreException 
91454      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: AssertionError, formerNode: AssertionError 
91456      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Character, formerNode: Character 
91457      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
91457      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
91459      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ClassCastException, formerNode: ClassCastException 
91460      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: CloneNotSupportedException, formerNode: CloneNotSupportedException 
91461      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cloneable, formerNode: Cloneable 
91462      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Comparable, formerNode: Comparable 
91463      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Double, formerNode: Double 
91465      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
91466      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
91469      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Error, formerNode: Error 
91471      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Exception, formerNode: Exception 
91474      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
91475      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
91476      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Float, formerNode: Float 
91480      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IllegalArgumentException, formerNode: IllegalArgumentException 
91481      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IndexOutOfBoundsException, formerNode: IndexOutOfBoundsException 
91500      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
91500      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
91502      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InterruptedException, formerNode: InterruptedException 
91503      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterable, formerNode: Iterable 
91504      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkageError, formerNode: LinkageError 
91514      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Math, formerNode: Math 
91516      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NegativeArraySizeException, formerNode: NegativeArraySizeException 
91520      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
91520      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
91521      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NullPointerException, formerNode: NullPointerException 
91522      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Number, formerNode: Number 
91524      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NumberFormatException, formerNode: NumberFormatException 
91525      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: VirtualMachineError, formerNode: VirtualMachineError 
91527      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutOfMemoryError, formerNode: OutOfMemoryError 
91527      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Runnable, formerNode: Runnable 
91529      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: RuntimeException, formerNode: RuntimeException 
91529      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
91532      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
91532      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
91542      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
91552      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
91572      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
91575      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: char, formerNode: /*@ helper */
char 
91577      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: StringBuffer, formerNode: StringBuffer 
91581      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: System, formerNode: System 
91582      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Thread, formerNode: Thread 
91585      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
91586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
91592      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Collection, formerNode: Collection 
91593      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
91593      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
91598      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
91598      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
91601      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
91601      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
91602      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Long, formerNode: Long 
91603      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Boolean, formerNode: Boolean 
91607      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Map, formerNode: Map 
91611      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
91612      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
91613      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: FilterOutputStream, formerNode: FilterOutputStream 
91614      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
91614      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
91617      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IOException, formerNode: IOException 
91618      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
91618      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
91623      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
91623      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
91624      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Serializable, formerNode: Serializable 
91625      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
91627      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
91628      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayList, formerNode: ArrayList 
91630      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
91652      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Arrays, formerNode: Arrays 
91653      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIteratorImpl, formerNode: ListIteratorImpl 
91654      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Date, formerNode: Date 
91655      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedHashMap, formerNode: LinkedHashMap 
91656      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: /*@strictly_pure*/
java.lang.String 
91657      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedList, formerNode: LinkedList 
91673      INFO  Test worker     d.u.i.k.n.KeyIO           Parsing took 1 ms 
91673      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 
91673      INFO  Test worker     d.u.i.k.n.KeyIO           MODE: declarations took 0 ms 
91673      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: 2nd degree decls took 0 
91682      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: taclets took 9ms