ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m9.84s

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] 2.737s 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] 2.752s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.773s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.798s 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] 2.767s 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] 2.767s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.766s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.766s 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] 2.737s 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] 2.797s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 2.857s 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] 2.751s 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] 2.735s 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] 2.751s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.814s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.799s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.766s 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] 2.931s 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] 2.908s 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] 2.886s 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] 2.845s 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] 2.831s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.783s 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] 2.783s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 2.736s passed

Standard output

664954     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 
664954     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 
664954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.7ns 
664954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
667706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
667706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
667815     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14231476030817535210.key 
667815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14231476030817535210.key 
667815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232ns 
667815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
670629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14231476030817535210.key 
670629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
670738     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 
670738     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 
670738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.3ns 
670738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
673506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
673537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.95ms 
673647     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9595051437989720156.key 
673647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9595051437989720156.key 
673647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 
673647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
676429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9595051437989720156.key 
676429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
676532     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17093133022131773198.key 
676532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17093133022131773198.key 
676532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242ns 
676532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
679268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17093133022131773198.key 
679268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
679378     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12318914560458424078.key 
679378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12318914560458424078.key 
679378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
679378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
682099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12318914560458424078.key 
682099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
682208     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15389710618724645656.key 
682208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15389710618724645656.key 
682208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
682208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
684882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15389710618724645656.key 
684882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
684992     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_486110036251094699.key 
684992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_486110036251094699.key 
684992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.9ns 
684992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
687665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_486110036251094699.key 
687665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
687775     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_7006644947786394232.key 
687775     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_7006644947786394232.key 
687775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.3ns 
687775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
690386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7006644947786394232.key 
690402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
690511     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13952468655038592637.key 
690511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13952468655038592637.key 
690511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.5ns 
690511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
693139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13952468655038592637.key 
693139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
693248     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 
693248     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 
693248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.3ns 
693248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
695891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
695891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
696000     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_10898873145708287480.key 
696000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_10898873145708287480.key 
696000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.7ns 
696000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
698658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_10898873145708287480.key 
698658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
698773     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17193358711149728903.key 
698773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17193358711149728903.key 
698773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.7ns 
698773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
701462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_17193358711149728903.key 
701462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
701571     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13451967450904789036.key 
701571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13451967450904789036.key 
701571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.9ns 
701571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
704229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13451967450904789036.key 
704229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
704339     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6574467909752548700.key 
704339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6574467909752548700.key 
704339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.5ns 
704339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
706996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6574467909752548700.key 
706996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
707105     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11350600568732639931.key 
707105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11350600568732639931.key 
707105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.9ns 
707105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
709764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_11350600568732639931.key 
709764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
709874     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9123939621819893139.key 
709874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9123939621819893139.key 
709874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.6ns 
709874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
712532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9123939621819893139.key 
712532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
712642     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11696843313273223457.key 
712642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11696843313273223457.key 
712642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.2ns 
712642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
715253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11696843313273223457.key 
715269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
715379     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13168841364854390807.key 
715379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13168841364854390807.key 
715379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 
715379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
718067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_13168841364854390807.key 
718067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
718176     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1843057721283775680.key 
718176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1843057721283775680.key 
718176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.2ns 
718176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
720818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1843057721283775680.key 
720818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
720928     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14845839393439193027.key 
720928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14845839393439193027.key 
720928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
720928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
723555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14845839393439193027.key 
723555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
723664     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_7833042165215752321.key 
723664     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_7833042165215752321.key 
723664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 
723664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
726306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_7833042165215752321.key 
726306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
726415     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15706667139483241381.key 
726415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15706667139483241381.key 
726415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331ns 
726415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
729105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15706667139483241381.key 
729121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
729230     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_1870236693941474882.key 
729230     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_1870236693941474882.key 
729230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.6ns 
729230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
731921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1870236693941474882.key 
731921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
732029     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13878217752254156542.key 
732029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13878217752254156542.key 
732029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222ns 
732029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
734687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_13878217752254156542.key 
734687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns