ProveSMTLemmasTest

all > de.uka.ilkd.key.smt.newsmt2 > ProveSMTLemmasTest
25

tests
0

failures
0

ignored
12.089s

duration
100%

successful

Tests

Test Method name Duration Result
[10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) testSMTLemmaSoundness(String, String)[10] 0.390s passed
[11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) testSMTLemmaSoundness(String, String)[11] 0.410s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 0.375s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 0.364s passed
[14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) testSMTLemmaSoundness(String, String)[14] 0.390s passed
[15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) testSMTLemmaSoundness(String, String)[15] 0.411s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 0.359s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 0.366s passed
[18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) testSMTLemmaSoundness(String, String)[18] 0.501s passed
[19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) testSMTLemmaSoundness(String, String)[19] 0.411s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 0.564s passed
[20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f)) testSMTLemmaSoundness(String, String)[20] 0.405s passed
[21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) testSMTLemmaSoundness(String, String)[21] 0.393s passed
[22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) testSMTLemmaSoundness(String, String)[22] 0.380s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 0.376s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 0.362s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 0.512s passed
[2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) testSMTLemmaSoundness(String, String)[2] 1.742s passed
[3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) testSMTLemmaSoundness(String, String)[3] 0.789s passed
[4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) testSMTLemmaSoundness(String, String)[4] 0.401s passed
[5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) testSMTLemmaSoundness(String, String)[5] 0.400s passed
[6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) testSMTLemmaSoundness(String, String)[6] 0.382s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 0.506s passed
[8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) testSMTLemmaSoundness(String, String)[8] 0.526s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 0.374s passed

Standard error

1015085    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 
1015085    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 
1015085    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
1015085    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1015225    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1015272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1015288    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1015303    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1015319    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1015382    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 284.42ms 
1015397    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1015527    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.04ms 
1015653    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1967179379048998076.key 
1015653    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1967179379048998076.key 
1015653    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
1015653    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1015793    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1015824    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1015824    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1015824    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1015824    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1015824    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1015840    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1015856    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1015856    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1015887    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1015934    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 279.65ms 
1015965    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1967179379048998076.key 
1015965    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
1017401    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 
1017401    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 
1017401    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.4ns 
1017406    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1017535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1017568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1017570    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1017571    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1017571    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1017572    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1017575    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1017592    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1017593    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1017624    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1017671    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 268.43ms 
1017687    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1018062    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 311.73ms 
1018188    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14450407473828165182.key 
1018188    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14450407473828165182.key 
1018188    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
1018188    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1018329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1018360    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1018391    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1018392    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1018408    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1018454    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 262.79ms 
1018470    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14450407473828165182.key 
1018486    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
1018595    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4416511768105953558.key 
1018595    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4416511768105953558.key 
1018595    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261ns 
1018595    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1018721    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1018753    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1018753    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1018753    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1018753    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1018753    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1018768    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1018784    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1018784    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1018815    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1018862    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 263.69ms 
1018878    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_4416511768105953558.key 
1018878    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
1018994    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_748248714695738410.key 
1018994    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_748248714695738410.key 
1018994    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271ns 
1018994    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1019121    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1019152    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1019152    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1019152    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1019152    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1019168    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1019168    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1019183    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1019183    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1019215    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1019246    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 255.44ms 
1019262    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_748248714695738410.key 
1019262    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1019378    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8123714489968113342.key 
1019378    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8123714489968113342.key 
1019378    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
1019378    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1019488    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1019519    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1019535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1019535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1019535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1019535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1019535    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1019551    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1019551    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1019582    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1019760    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 380.91ms 
1019775    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8123714489968113342.key 
1019775    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
1019885    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13396961429799836641.key 
1019885    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13396961429799836641.key 
1019885    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
1019885    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1020023    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1020187    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1020203    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1020203    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1020234    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1020281    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 394.15ms 
1020296    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13396961429799836641.key 
1020296    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
1020412    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_16676354583593306148.key 
1020412    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_16676354583593306148.key 
1020412    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 
1020412    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1020522    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1020568    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1020584    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1020584    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1020615    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1020647    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 245.56ms 
1020678    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_16676354583593306148.key 
1020678    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
1020787    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1806004211837161210.key 
1020787    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1806004211837161210.key 
1020787    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 
1020787    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1020896    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1020928    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1020943    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1020943    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1020943    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1020943    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1020943    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1020959    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1020959    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1020990    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1021037    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 249.86ms 
1021053    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_1806004211837161210.key 
1021053    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1021178    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 
1021178    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 
1021178    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
1021178    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1021287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1021318    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1021334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1021334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1021334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1021334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1021334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1021350    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1021350    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1021381    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1021428    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 257.74ms 
1021459    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1021475    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
1021584    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14085779204382579058.key 
1021584    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14085779204382579058.key 
1021584    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.3ns 
1021584    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1021694    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1021741    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1021756    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1021756    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1021787    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1021834    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 241.81ms 
1021850    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14085779204382579058.key 
1021854    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
1021964    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15270552998220825007.key 
1021964    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15270552998220825007.key 
1021964    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
1021964    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1022074    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1022105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1022120    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1022120    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1022120    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1022120    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1022120    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1022136    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1022136    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1022167    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1022199    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 241.8ms 
1022214    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15270552998220825007.key 
1022214    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
1022329    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2407811820606846118.key 
1022329    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2407811820606846118.key 
1022329    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.7ns 
1022329    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1022439    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1022470    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1022485    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1022485    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1022485    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1022485    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1022485    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1022501    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1022501    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1022539    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1022579    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 257.68ms 
1022611    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2407811820606846118.key 
1022611    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
1022720    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9051696975599688706.key 
1022720    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9051696975599688706.key 
1022720    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.1ns 
1022720    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1022845    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1022876    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1022876    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1022876    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1022876    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1022876    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1022891    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1022911    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1022914    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1022938    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1022985    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 266.79ms 
1023016    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9051696975599688706.key 
1023016    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
1023131    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9007472795593033059.key 
1023131    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9007472795593033059.key 
1023131    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.8ns 
1023131    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1023240    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1023272    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1023287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1023287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1023287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1023287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1023287    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1023303    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1023303    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1023334    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1023365    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 239.17ms 
1023381    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9007472795593033059.key 
1023381    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
1023491    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15174631695264752244.key 
1023491    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15174631695264752244.key 
1023491    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.8ns 
1023491    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1023601    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1023648    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1023663    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1023663    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1023695    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1023726    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 242.84ms 
1023741    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15174631695264752244.key 
1023741    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
1023858    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12208841675166816289.key 
1023858    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12208841675166816289.key 
1023858    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.3ns 
1023858    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1023979    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1024026    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1024042    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1024042    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1024073    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1024220    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 368.58ms 
1024251    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_12208841675166816289.key 
1024251    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
1024360    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8389780633427568418.key 
1024360    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8389780633427568418.key 
1024360    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.7ns 
1024360    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1024470    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1024501    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1024517    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1024517    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1024517    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1024517    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1024517    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1024533    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1024533    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1024564    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1024611    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 258.96ms 
1024642    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8389780633427568418.key 
1024658    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
1024767    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7746725512733814880.key 
1024767    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7746725512733814880.key 
1024767    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
1024767    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1024892    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1024933    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1024948    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1024948    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1024980    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1025026    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 265.51ms 
1025058    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7746725512733814880.key 
1025058    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1025173    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9133749505661150206.key 
1025173    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9133749505661150206.key 
1025173    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.7ns 
1025173    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1025283    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1025329    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1025345    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1025345    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1025376    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1025423    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 257.27ms 
1025455    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9133749505661150206.key 
1025455    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1025567    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_17198592076353494468.key 
1025567    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_17198592076353494468.key 
1025567    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184ns 
1025567    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1025677    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1025724    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1025739    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1025739    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1025770    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1025817    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 250.62ms 
1025833    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17198592076353494468.key 
1025833    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
1025949    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10426254335874073123.key 
1025949    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10426254335874073123.key 
1025949    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.8ns 
1025949    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1026074    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1026105    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1026137    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1026137    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1026153    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1026200    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 250.02ms 
1026216    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_10426254335874073123.key 
1026216    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
1026325    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_13160429648144349061.key 
1026325    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_13160429648144349061.key 
1026325    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
1026325    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1026434    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1026466    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1026481    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1026481    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1026481    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1026481    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1026481    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1026497    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1026497    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1026528    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1026560    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 239.61ms 
1026576    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13160429648144349061.key 
1026576    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1026688    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1383862176694676041.key 
1026688    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1383862176694676041.key 
1026688    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
1026688    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1026813    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
1026844    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
1026844    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
1026844    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
1026844    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
1026844    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
1026984    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
1027010    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
1027010    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
1027042    ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
1027073    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 388.78ms 
1027088    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1383862176694676041.key 
1027088    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns