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.321s | 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.137s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.334s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.216s | 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.269s | 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.302s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.282s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.366s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 3.338s | 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.226s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.277s | 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.287s | 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.237s | 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.303s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.308s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.373s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.189s | 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.290s | 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.507s | 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.429s | 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.485s | 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.230s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.267s | 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.245s | 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.369s | passed |
Standard output
778059 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 778059 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 778059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 778059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 781210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 781225 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 781335 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5037041567426150783.key 781335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5037041567426150783.key 781335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.7ns 781335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 784493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 784508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_5037041567426150783.key 784508 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 784625 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 784625 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 784625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.2ns 784625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 787923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 787955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 788017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.09ms 788132 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7070943796057249032.key 788132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7070943796057249032.key 788132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.2ns 788132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 791437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7070943796057249032.key 791453 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.1ns 791562 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14523499542540386115.key 791562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14523499542540386115.key 791562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.1ns 791562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 794937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14523499542540386115.key 794937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 795047 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5483099612843887804.key 795047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5483099612843887804.key 795047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250ns 795047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 798168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_5483099612843887804.key 798168 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 798277 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10985940232525982113.key 798277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10985940232525982113.key 798277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.6ns 798277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 801436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10985940232525982113.key 801436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 801545 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_12767797295732737916.key 801545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_12767797295732737916.key 801545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.1ns 801545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 804678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_12767797295732737916.key 804678 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 804790 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_11749977582635540979.key 804790 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_11749977582635540979.key 804790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.5ns 804790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 808034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11749977582635540979.key 808034 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 808159 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2638913467868723043.key 808159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2638913467868723043.key 808159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.93ms 808159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811350 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 811365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_2638913467868723043.key 811365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 811480 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 811480 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 811480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.5ns 811480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 814485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 814501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 814501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 814617 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7435297133596428142.key 814617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7435297133596428142.key 814617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.8ns 814617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 817842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7435297133596428142.key 817842 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 817952 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_18395345570006300929.key 817952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_18395345570006300929.key 817952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.4ns 817952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 821059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_18395345570006300929.key 821059 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 821169 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12414672248682500597.key 821169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12414672248682500597.key 821169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.7ns 821169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 824326 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12414672248682500597.key 824326 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 824438 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7798122288985856407.key 824438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7798122288985856407.key 824438 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.8ns 824438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 827628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7798122288985856407.key 827628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 827740 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1437358963003449226.key 827740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1437358963003449226.key 827740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 516ns 827740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 830866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_1437358963003449226.key 830898 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 831023 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13552744166738342695.key 831023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13552744166738342695.key 831023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 831023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 834280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13552744166738342695.key 834280 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 834389 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3106814250600248547.key 834389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3106814250600248547.key 834389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 834389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 837617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3106814250600248547.key 837617 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ns 837727 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4481244463937747672.key 837727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4481244463937747672.key 837727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.8ns 837727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 840844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4481244463937747672.key 840844 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 840954 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9874794460503328749.key 840954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9874794460503328749.key 840954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.3ns 840954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844116 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 844131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9874794460503328749.key 844131 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 844241 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_283071759842439361.key 844241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_283071759842439361.key 844241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 844241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 847368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_283071759842439361.key 847368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 847478 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_10710049817569439340.key 847478 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_10710049817569439340.key 847478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 847478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 850655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10710049817569439340.key 850671 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 850781 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11965748761035448920.key 850781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11965748761035448920.key 850781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.4ns 850781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 853973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11965748761035448920.key 853973 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 854089 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_12848999909708249005.key 854089 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_12848999909708249005.key 854089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.3ns 854089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 857349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12848999909708249005.key 857349 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 857463 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7929355687292877490.key 857463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7929355687292877490.key 857463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 857463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 860539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7929355687292877490.key 860539 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns