ProveSMTLemmasTest

25

tests

0

failures

0

ignored

1m32.55s

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] 3.673s 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] 3.673s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.690s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.690s 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] 3.674s 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] 3.660s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.658s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.675s 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] 3.704s 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] 3.675s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 3.796s 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] 3.677s 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] 3.691s 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] 3.689s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.689s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.735s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.627s 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] 3.799s 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] 3.830s 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] 3.783s 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] 3.801s 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] 3.736s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.658s 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] 3.627s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 3.643s passed

Standard output

876751     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 
876751     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 
876751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
876751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
880409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
880440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
880440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.13ms 
880549     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8961096152376746908.key 
880549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8961096152376746908.key 
880549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.2ns 
880549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
884239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8961096152376746908.key 
884239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.1ns 
884349     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 
884349     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 
884349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333ns 
884349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
888023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
888038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
888069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.95ms 
888179     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11593385571972689351.key 
888179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11593385571972689351.key 
888179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.8ns 
888179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
891822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
891837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11593385571972689351.key 
891853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
891962     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_328947378969582238.key 
891962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_328947378969582238.key 
891962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.9ns 
891962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
895623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
895638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_328947378969582238.key 
895638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
895763     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13400536647534492607.key 
895763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13400536647534492607.key 
895763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 
895763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
899359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
899390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13400536647534492607.key 
899390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
899499     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2222128977624624205.key 
899499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2222128977624624205.key 
899499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.3ns 
899499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
903018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
903033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2222128977624624205.key 
903033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
903158     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9297305219968083416.key 
903158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9297305219968083416.key 
903158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
903158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
906660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
906675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9297305219968083416.key 
906675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 
906785     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_6112371936196060631.key 
906785     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_6112371936196060631.key 
906785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.5ns 
906785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
910303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
910319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_6112371936196060631.key 
910319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
910428     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5906837214842773542.key 
910428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5906837214842773542.key 
910428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.6ns 
910428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
913976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
913992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5906837214842773542.key 
913992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
914101     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 
914101     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 
914101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
914101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
917603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
917635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
917650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.81ms 
917775     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12279529297728530264.key 
917775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12279529297728530264.key 
917775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.7ns 
917775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
921340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
921356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12279529297728530264.key 
921356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
921465     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6396931138377678977.key 
921465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6396931138377678977.key 
921465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.9ns 
921465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
925015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
925046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6396931138377678977.key 
925046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
925155     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17256243543901068656.key 
925155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17256243543901068656.key 
925155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.4ns 
925155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
928703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
928719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17256243543901068656.key 
928719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
928829     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_841842382178916988.key 
928829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_841842382178916988.key 
928829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.9ns 
928829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
932348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
932364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_841842382178916988.key 
932379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
932489     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_557975964707463235.key 
932489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_557975964707463235.key 
932489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249ns 
932489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
936023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
936039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_557975964707463235.key 
936039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
936148     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3996401535099610685.key 
936148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3996401535099610685.key 
936148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.1ns 
936148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
939698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
939713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3996401535099610685.key 
939713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
939823     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2960859614745956931.key 
939823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2960859614745956931.key 
939823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.9ns 
939823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
943403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
943419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2960859614745956931.key 
943419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 
943528     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14625850596506107713.key 
943528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14625850596506107713.key 
943528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.5ns 
943528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
947078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
947094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14625850596506107713.key 
947094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
947203     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4885708867556923669.key 
947203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4885708867556923669.key 
947203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.81ms 
947203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
950736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
950752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4885708867556923669.key 
950768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
950880     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12482905115803753069.key 
950880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12482905115803753069.key 
950880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.72ms 
950880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
954430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
954461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12482905115803753069.key 
954461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
954571     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_2899011844127356215.key 
954571     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_2899011844127356215.key 
954571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.4ns 
954571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
958135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
958151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2899011844127356215.key 
958151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
958260     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16313562975638113957.key 
958260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16313562975638113957.key 
958260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
958260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
961808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
961824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16313562975638113957.key 
961840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
961949     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_14598021964807647927.key 
961949     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_14598021964807647927.key 
961949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.5ns 
961949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
965563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
965579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14598021964807647927.key 
965579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
965689     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1485019176810701804.key 
965689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1485019176810701804.key 
965689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.2ns 
965689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
969191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
969207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1485019176810701804.key 
969207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns