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] | 4.141s | 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.830s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.877s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.895s | 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.784s | 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] | 4.947s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.782s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.743s | 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.705s | 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.659s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.765s | 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.627s | 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.470s | 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.533s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.470s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.658s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.628s | 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.828s | 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.799s | 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.673s | 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.549s | 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.767s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.706s | 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.690s | 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.830s | passed |
Standard output
754352 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 754352 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 754352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms 754352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 757948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 757964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 757995 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.17ms 758105 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6364490574456496860.key 758105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6364490574456496860.key 758105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.7ns 758105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 761793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 761809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6364490574456496860.key 761809 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 761934 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 761934 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 761934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.9ns 761934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 765530 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 765546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 765624 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.06ms 765734 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16387918933280219571.key 765734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16387918933280219571.key 765734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.3ns 765734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 769297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16387918933280219571.key 769297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 769407 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14294152579487523993.key 769407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14294152579487523993.key 769407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.6ns 769407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 772846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14294152579487523993.key 772846 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 772956 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15614326277382607519.key 772956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15614326277382607519.key 772956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.5ns 772956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 776599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 776615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15614326277382607519.key 776615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 776724 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11562381948273877372.key 776724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11562381948273877372.key 776724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.9ns 776724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 780321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_11562381948273877372.key 780321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ns 780430 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17256028630867900096.key 780430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17256028630867900096.key 780430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.9ns 780430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 783980 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 783996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17256028630867900096.key 784012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 784121 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_11217727070071690385.key 784121 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_11217727070071690385.key 784121 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.6ns 784121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 787826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 787841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11217727070071690385.key 787841 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 787952 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_314437877558322735.key 787952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_314437877558322735.key 787952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 787952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 791593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_314437877558322735.key 791593 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 792093 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 792093 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 792093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 792093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 795798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 795813 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.88ms 795923 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5263402038218972143.key 795923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5263402038218972143.key 795923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.2ns 795923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 799690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5263402038218972143.key 799690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 799800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11133297037584814277.key 799800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11133297037584814277.key 799800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 551.2ns 799800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 803556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 803571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11133297037584814277.key 803587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 803696 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10007093649283895852.key 803696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10007093649283895852.key 803696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.2ns 803696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 807371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10007093649283895852.key 807371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 807496 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6748385443719482618.key 807496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6748385443719482618.key 807496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.6ns 807496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 811373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6748385443719482618.key 811373 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 812436 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3528296921108750078.key 812436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3528296921108750078.key 812436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.8ns 812436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 816095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3528296921108750078.key 816095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.2ns 816345 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11621500930193706617.key 816345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11621500930193706617.key 816345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.5ns 816345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 819972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11621500930193706617.key 819972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 820081 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10340226072928560642.key 820081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10340226072928560642.key 820081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.4ns 820081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 823677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10340226072928560642.key 823677 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 823786 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16972063283885464907.key 823786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16972063283885464907.key 823786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 392ns 823786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 827335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_16972063283885464907.key 827335 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 827445 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9694581337881961856.key 827445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9694581337881961856.key 827445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.7ns 827445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 830964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9694581337881961856.key 830964 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 831073 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16591454832842785190.key 831073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16591454832842785190.key 831073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 611.5ns 831073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 834435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16591454832842785190.key 834435 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 834544 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_18209468687432668547.key 834544 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_18209468687432668547.key 834544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.6ns 834544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 837968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_18209468687432668547.key 837968 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 838077 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17765399287741008290.key 838077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17765399287741008290.key 838077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 529.4ns 838077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 841438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17765399287741008290.key 841438 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 841548 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_13616648819350660166.key 841548 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_13616648819350660166.key 841548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.7ns 841548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 845098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13616648819350660166.key 845098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 845207 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17937556906156536339.key 845207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17937556906156536339.key 845207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.4ns 845207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 848710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17937556906156536339.key 848710 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns