31300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/key-focus-command15458375999065109027.key
31300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.71ns
31303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
31408 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean
31452 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure*/
int, formerNode: int
31455 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
int, formerNode: int
31455 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean
31456 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
char, formerNode: char
31457 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: byte[], formerNode: byte[]
31460 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String
31480 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String
31484 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object
31520 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure@*/
String, formerNode: String
31563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 259.94ms
31599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof key-focus-command15458375999065109027.key
31605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns
31607 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro 'nosplit-prop''
31661 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 1, command: 'focus 'i=1 ==> i = 3''
31681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/key-focus-command2675930836693766489.key
31681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.11ns
31682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
31789 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean
31926 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure*/
int, formerNode: int
31929 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
int, formerNode: int
31929 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean
31929 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
char, formerNode: char
31930 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: byte[], formerNode: byte[]
31934 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String
31952 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String
31956 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object
31988 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure@*/
String, formerNode: String
32027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 344.92ms
32057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof key-focus-command2675930836693766489.key
32059 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns
32060 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro 'nosplit-prop''
32074 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 1, command: 'focus 'i=1 ==> i = 4''