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.653s | 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] | 4.032s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.622s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.522s | 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.737s | 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.596s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.575s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.737s | 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.788s | 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] | 4.011s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.848s | 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.615s | 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.573s | 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.614s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.634s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.491s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.618s | 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.577s | 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.836s | 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.643s | 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.834s | 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.651s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.761s | 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.601s | 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.591s | passed |
Standard output
865655 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 865655 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 865655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 865671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 869375 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 869375 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 869490 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_3047711317553388719.key 869490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_3047711317553388719.key 869490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 869490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 872957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_3047711317553388719.key 872957 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 873067 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 873067 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 873067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 873067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 876731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 876746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 876778 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.53ms 876903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11831726093786230323.key 876903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11831726093786230323.key 876903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.8ns 876903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 880437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11831726093786230323.key 880437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 880546 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13313237395978919369.key 880546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13313237395978919369.key 880546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.8ns 880546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 884267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13313237395978919369.key 884267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 884380 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12925941916813775406.key 884380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12925941916813775406.key 884380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161ns 884380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 887922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12925941916813775406.key 887922 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 888031 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17234508494683769182.key 888031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17234508494683769182.key 888031 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 888031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 891683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17234508494683769182.key 891683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 891792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6164385872791080353.key 891792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6164385872791080353.key 891792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 891792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 895278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6164385872791080353.key 895278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 895393 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_18383221087292566352.key 895393 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_18383221087292566352.key 895393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.5ns 895393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 898875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_18383221087292566352.key 898875 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 898984 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14127874416425334895.key 898984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14127874416425334895.key 898984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.1ns 898984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 902521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_14127874416425334895.key 902521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 902637 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 902637 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 902637 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 902637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 906210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 906553 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.82ms 906669 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16977057633211778579.key 906669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16977057633211778579.key 906669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.4ns 906669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 910167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 910183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_16977057633211778579.key 910183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 910292 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8206121364635547567.key 910292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8206121364635547567.key 910292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.9ns 910292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 913699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8206121364635547567.key 913699 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 913814 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13163126281814058332.key 913814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13163126281814058332.key 913814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.6ns 913814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 917426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 917443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13163126281814058332.key 917443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 917551 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16905490060442206811.key 917551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16905490060442206811.key 917551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.3ns 917551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 921023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 921038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_16905490060442206811.key 921038 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 921147 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15726427806050893180.key 921147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15726427806050893180.key 921147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.8ns 921147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 924592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 924608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_15726427806050893180.key 924608 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 924723 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17505266113852452118.key 924723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17505266113852452118.key 924723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.4ns 924723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 928273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 928288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17505266113852452118.key 928288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 928460 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18194921502308362306.key 928460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18194921502308362306.key 928460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.8ns 928460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 932118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 932134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18194921502308362306.key 932134 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 932248 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3027084792001118841.key 932248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3027084792001118841.key 932248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.8ns 932248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 936127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 936143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3027084792001118841.key 936143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 936259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2622275212801142617.key 936259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2622275212801142617.key 936259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 936259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 939745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 939762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2622275212801142617.key 939762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 939874 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3800301286322043283.key 939874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3800301286322043283.key 939874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 939874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 943317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 943333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3800301286322043283.key 943333 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 943447 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_17537548145451644568.key 943447 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_17537548145451644568.key 943447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 943447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 946934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17537548145451644568.key 946948 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 947061 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15019673771684716802.key 947061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15019673771684716802.key 947061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.5ns 947061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 950580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15019673771684716802.key 950580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 950711 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_10025197997152678942.key 950711 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_10025197997152678942.key 950711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 950742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 954062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 954078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10025197997152678942.key 954078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 954191 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3481165369651485882.key 954191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3481165369651485882.key 954191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 954191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 957685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 957701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3481165369651485882.key 957701 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns