94474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\key-focus-command11367536985534215663.key
94474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 473.2ns
94474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
94599 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean
94630 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure*/
int, formerNode: int
94630 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
int, formerNode: int
94630 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean
94630 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
char, formerNode: char
94646 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: byte[], formerNode: byte[]
94646 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String
94668 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String
94668 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object
94700 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure@*/
String, formerNode: String
94731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 259.5ms
94778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof key-focus-command11367536985534215663.key
94778 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns
94778 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro 'nosplit-prop''
94856 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 1, command: 'focus 'i=1 ==> i = 3''
94920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\key-focus-command1351495434469955391.key
94920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns
94922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
95031 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean
95062 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure*/
int, formerNode: int
95078 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
int, formerNode: int
95078 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean
95078 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
char, formerNode: char
95078 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: byte[], formerNode: byte[]
95078 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String
95093 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String
95093 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object
95203 ERROR Test worker d.u.i.k.j.KeYJPMapping Duplicate registration of node: /*@pure@*/
String, formerNode: String
95250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 335.63ms
95281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof key-focus-command1351495434469955391.key
95297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns
95297 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro 'nosplit-prop''
95328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 1, command: 'focus 'i=1 ==> i = 4''