ProveSMTLemmasTest

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

tests
0

failures
0

ignored
10.569s

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.392s 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.427s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 0.471s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 0.367s 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.393s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 0.510s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 0.362s 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.399s 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.409s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 0.418s 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.538s 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.375s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 0.361s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 0.449s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 0.365s 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] 0.488s 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.644s 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.399s passed
[5] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) testSMTLemmaSoundness(String, String)[5] 0.378s passed
[6] 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)[6] 0.388s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 0.374s 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.502s 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.377s passed

Standard error

101215     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
101215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
101215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
101216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101342     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
101377     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
101379     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
101379     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
101379     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
101380     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
101383     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
101401     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
101405     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
101437     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
101484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 267.79ms 
101506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
101525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
101633     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_16521188715047417273.key 
101634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_16521188715047417273.key 
101634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
101634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101753     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
101788     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
101790     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
101790     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
101791     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
101792     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
101795     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
101813     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
101817     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
101848     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
101895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 260.61ms 
101918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16521188715047417273.key 
101919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
102122     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
102122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
102122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
102123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102245     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
102281     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
102283     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
102284     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
102284     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
102285     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
102288     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
102307     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
102311     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
102343     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
102527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 404.42ms 
102554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
102657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.8ms 
102767     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_14736780146432418408.key 
102768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_14736780146432418408.key 
102768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.6ns 
102769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102895     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
102934     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
102937     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
102937     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
102937     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
102939     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
102942     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
102961     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
102965     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
102997     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
103043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 274.19ms 
103062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14736780146432418408.key 
103064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 
103167     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_11280911660832123672.key 
103167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_11280911660832123672.key 
103167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
103168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103286     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
103321     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
103323     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
103323     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
103323     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
103324     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
103327     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
103345     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
103349     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
103380     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
103424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 256.37ms 
103441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_11280911660832123672.key 
103443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
103546     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_12446461132456376559.key 
103546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_12446461132456376559.key 
103546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
103546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103662     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
103698     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
103700     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
103700     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
103700     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
103701     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
103704     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
103722     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
103726     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
103757     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
103805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 258.88ms 
103830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12446461132456376559.key 
103831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
103934     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_12025149971126401518.key 
103934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_12025149971126401518.key 
103934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
103935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104056     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
104092     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
104094     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
104095     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
104095     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
104097     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
104100     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
104120     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
104124     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
104156     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
104192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 256.42ms 
104204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12025149971126401518.key 
104205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
104308     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_236003212831583422.key 
104308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_236003212831583422.key 
104308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
104309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104543     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
104578     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
104580     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
104581     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
104581     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
104582     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
104585     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
104602     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
104606     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
104637     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
104682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 373.61ms 
104704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_236003212831583422.key 
104706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
104810     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_3066196440204353007.key 
104811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_3066196440204353007.key 
104811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
104811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104929     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
104966     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
104968     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
104968     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
104968     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
104969     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
104972     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
104991     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
104994     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
105027     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
105067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 255.8ms 
105084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3066196440204353007.key 
105085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
105188     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_1220912589747615982.key 
105188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_1220912589747615982.key 
105189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 726.81ns 
105190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105309     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
105345     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
105347     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
105348     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
105348     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
105349     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
105352     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
105370     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
105373     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
105405     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
105453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 263.11ms 
105476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_1220912589747615982.key 
105478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
105580     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
105581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
105581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
105582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105708     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
105745     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
105747     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
105747     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
105747     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
105748     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
105752     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
105770     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
105774     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
105806     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
105863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 281.13ms 
105893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
105900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
106008     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_17467914413633944273.key 
106009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_17467914413633944273.key 
106009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
106009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106227     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
106262     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
106263     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
106264     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
106264     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
106265     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
106268     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
106285     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
106289     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
106320     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
106356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 347.04ms 
106376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17467914413633944273.key 
106377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
106480     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_5017240929307640648.key 
106481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_5017240929307640648.key 
106481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
106481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106598     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
106633     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
106635     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
106635     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
106635     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
106636     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
106639     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
106657     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
106661     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
106692     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
106729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 248.17ms 
106743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5017240929307640648.key 
106745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
106848     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_11820662272929315148.key 
106848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_11820662272929315148.key 
106848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
106849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106967     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
107003     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
107008     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
107008     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
107008     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
107009     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
107012     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
107030     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
107033     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
107065     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
107111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 262.43ms 
107134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11820662272929315148.key 
107136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
107239     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_12163489171220464881.key 
107239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_12163489171220464881.key 
107239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
107240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107354     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
107390     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
107391     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
107392     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
107392     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
107393     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
107396     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
107413     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
107417     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
107448     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
107500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 259.97ms 
107528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12163489171220464881.key 
107530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
107634     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_5627957012477344806.key 
107634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_5627957012477344806.key 
107634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.9ns 
107635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107890     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
107927     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
107929     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
107930     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
107931     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
107932     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
107935     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
107953     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
107957     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
107989     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
108026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 391.16ms 
108038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5627957012477344806.key 
108041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
108143     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_12862034235183502728.key 
108144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_12862034235183502728.key 
108144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
108145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108259     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
108294     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
108296     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
108296     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
108297     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
108297     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
108300     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
108318     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
108322     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
108353     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
108389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 244.63ms 
108401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12862034235183502728.key 
108403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 
108506     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_7360825008533121927.key 
108506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_7360825008533121927.key 
108506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
108507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108634     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
108672     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
108674     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
108674     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
108675     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
108676     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
108679     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
108698     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
108702     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
108734     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
108778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 270.85ms 
108800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7360825008533121927.key 
108804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
108906     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_9821122348412382096.key 
108906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_9821122348412382096.key 
108907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
108908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109029     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
109064     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
109066     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
109066     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
109067     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
109068     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
109070     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
109088     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
109092     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
109123     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
109179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 271.66ms 
109211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_9821122348412382096.key 
109213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 
109316     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_17160821459109730690.key 
109316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_17160821459109730690.key 
109316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
109318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109563     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
109603     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
109605     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
109606     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
109606     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
109608     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
109611     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
109631     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
109635     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
109666     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
109719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 400.63ms 
109747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17160821459109730690.key 
109749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 
109855     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_15221042362287512362.key 
109855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_15221042362287512362.key 
109855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
109856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109972     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
110007     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
110009     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
110009     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
110009     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
110010     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
110013     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
110031     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
110035     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
110066     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
110116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 260.75ms 
110144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_15221042362287512362.key 
110145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
110248     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_13501415922403028506.key 
110248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_13501415922403028506.key 
110249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235ns 
110249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110364     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
110400     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
110401     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
110402     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
110402     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
110403     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
110406     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
110425     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
110429     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
110460     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
110501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 252.19ms 
110520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13501415922403028506.key 
110521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
110624     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_8637371863749852208.key 
110624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_8637371863749852208.key 
110624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
110625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110738     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
110773     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
110775     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
110775     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
110775     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
110776     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
110779     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
110797     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
110800     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
110831     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
110868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 243.41ms 
110881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8637371863749852208.key 
110883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
110985     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_17842108431826486615.key 
110986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_17842108431826486615.key 
110986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
110986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111191     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
111225     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
111227     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
111227     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
111227     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
111228     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
111231     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
111249     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
111252     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
111283     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
111318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 332.21ms 
111331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17842108431826486615.key 
111333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
111435     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_149282783797560800.key 
111435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_149282783797560800.key 
111436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
111436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111550     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
111585     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
111587     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
111587     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
111587     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
111588     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
111591     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
111609     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
111612     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
111644     ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
111682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 245.93ms 
111696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_149282783797560800.key 
111698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns