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.290s | 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.221s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.283s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.413s | 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.295s | 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.376s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.188s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.215s | 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.287s | 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.237s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.383s | 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.320s | 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.240s | 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.333s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.265s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.256s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.265s | 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.173s | 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.502s | 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.227s | 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.211s | 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.346s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.746s | 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.226s | 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.373s | passed |
Standard output
765967 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 765967 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 765967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 765967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769192 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 769223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 769223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 769334 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8850801686098516152.key 769334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8850801686098516152.key 769334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 769334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 772382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8850801686098516152.key 772382 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 772507 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 772507 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 772507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.4ns 772507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 775857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 775897 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.76ms 776009 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3313396974757837328.key 776009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3313396974757837328.key 776009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.8ns 776009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 779104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 779120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3313396974757837328.key 779120 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 243.5ns 779236 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14851293911144077102.key 779236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14851293911144077102.key 779236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145ns 779236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 782318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 782334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14851293911144077102.key 782334 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 782447 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4874310229062254640.key 782447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4874310229062254640.key 782447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 782447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 785606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4874310229062254640.key 785606 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 785814 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10967200221289820895.key 785814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10967200221289820895.key 785814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150ns 785817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789414 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 789430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10967200221289820895.key 789430 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 789540 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_12128868146750437176.key 789540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_12128868146750437176.key 789540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 789540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 792641 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 792656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_12128868146750437176.key 792656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 792767 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_15887532078971043687.key 792767 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_15887532078971043687.key 792767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.5ns 792767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 796031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15887532078971043687.key 796031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 796140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15840716261217216593.key 796140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15840716261217216593.key 796140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.8ns 796140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 799320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15840716261217216593.key 799325 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 799430 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 799430 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 799430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.7ns 799430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 802535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 802535 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 802651 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8381948203226395091.key 802651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8381948203226395091.key 802651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 802651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 805825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8381948203226395091.key 805825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 805935 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9340309344764506203.key 805935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9340309344764506203.key 805935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 805935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 809233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9340309344764506203.key 809233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ns 809348 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11688484778254815241.key 809348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11688484778254815241.key 809348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.6ns 809348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 812525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11688484778254815241.key 812525 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 812644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7558862494729739694.key 812644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7558862494729739694.key 812644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.3ns 812644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815894 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 815910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7558862494729739694.key 815910 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 816022 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12429419963046164469.key 816022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12429419963046164469.key 816022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.4ns 816022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 819102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12429419963046164469.key 819102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 819211 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4411164167029537835.key 819211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4411164167029537835.key 819211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 819211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 822315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4411164167029537835.key 822315 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 822426 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3257226678811921275.key 822426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3257226678811921275.key 822426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns 822426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 825603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3257226678811921275.key 825603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns 825713 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16839318301443921654.key 825713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16839318301443921654.key 825713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 825713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 828824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_16839318301443921654.key 828840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 828951 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8476154367653807621.key 828951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8476154367653807621.key 828951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.2ns 828951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 832156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8476154367653807621.key 832156 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 832271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3288397297031386362.key 832271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3288397297031386362.key 832271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.9ns 832271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 835386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3288397297031386362.key 835401 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 835511 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_1071568690380470420.key 835511 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_1071568690380470420.key 835511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 835511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 838734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1071568690380470420.key 838734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 838844 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3678073009264820229.key 838844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3678073009264820229.key 838844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 838844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 841994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3678073009264820229.key 841994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 842109 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_16514430655109033922.key 842109 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_16514430655109033922.key 842109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.68ms 842109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 845257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_16514430655109033922.key 845257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 845366 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12813675579936044934.key 845366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12813675579936044934.key 845366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 845366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 848522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12813675579936044934.key 848522 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns