RewriteTest

2

tests

0

failures

0

ignored

0.571s

duration

100%

successful

Tests

Test Duration Result
testLessTransitive() 0.289s passed
testTransitive() 0.282s passed

Standard error

34477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/scriptCommands/less_trans.key 
34478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.5ms 
34479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34589      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
34628      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
34631      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
34631      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
34632      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
34633      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
34636      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
34655      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
34659      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
34693      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
34733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 254.4ms 
34752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof less_trans.key 
34755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
34758      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rewrite find="f < x" replace="x > f"' 
34766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/scriptCommands/transitive.key 
34766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.81ns 
34767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34877      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
34914      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
34916      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
34917      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
34917      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
34919      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
34922      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
34941      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
34945      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
34978      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
35018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 251.16ms 
35037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof transitive.key 
35039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
35040      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule impRight' 
35043      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'rule andLeft' 
35046      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 2, source line: 3, command: 'rewrite find="f = x" replace="x = f"'