ProveSMTLemmasTest
|
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