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.253s | 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.346s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.503s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.502s | 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.454s | 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.424s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.345s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.345s | 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.613s | 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.691s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.415s | 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.112s | 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.174s | 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.142s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.282s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.271s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.440s | 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.471s | 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.472s | 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.565s | 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.609s | 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.534s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.486s | 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.487s | 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.658s | passed |
Standard output
822934 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 822934 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 822934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 822934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 826201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 826217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 826232 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 826342 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12563914931047056405.key 826342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12563914931047056405.key 826342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 826342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 829688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_12563914931047056405.key 829703 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 829813 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 829813 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 829813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.1ns 829813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 833144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 833176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.24ms 833285 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9037900168590429410.key 833285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9037900168590429410.key 833285 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.8ns 833285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 836724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 836740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9037900168590429410.key 836740 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.4ns 836850 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16077657967518991652.key 836850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16077657967518991652.key 836850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.4ns 836850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 840351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16077657967518991652.key 840351 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 840460 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16727713032694534751.key 840460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16727713032694534751.key 840460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.2ns 840460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 843853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 843884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_16727713032694534751.key 843884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 843994 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13335051680805243510.key 843994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13335051680805243510.key 843994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 843994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 847371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13335051680805243510.key 847371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 847480 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14880781264316184726.key 847480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14880781264316184726.key 847480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.9ns 847480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 850842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_14880781264316184726.key 850857 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ns 850967 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_1400251205601955648.key 850967 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_1400251205601955648.key 850967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353ns 850967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 854516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1400251205601955648.key 854516 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 854626 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14915021822437049745.key 854626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14915021822437049745.key 854626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns 854626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 857769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_14915021822437049745.key 857769 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 857879 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 857879 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 857879 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.9ns 857879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 861085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 861116 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 861116 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 861225 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14942089734682875683.key 861225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14942089734682875683.key 861225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.4ns 861225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 864619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14942089734682875683.key 864619 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 864728 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8424864593441292055.key 864728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8424864593441292055.key 864728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.4ns 864728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 868105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 868120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8424864593441292055.key 868120 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 868230 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4496854289235482069.key 868230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4496854289235482069.key 868230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.9ns 868230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 871575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_4496854289235482069.key 871575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 871684 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_704898290417431250.key 871684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_704898290417431250.key 871684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.9ns 871684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 874983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_704898290417431250.key 874999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 875108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13400011378486693546.key 875108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13400011378486693546.key 875108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.6ns 875108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 878345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13400011378486693546.key 878345 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 878454 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8453719855824096461.key 878454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8453719855824096461.key 878454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.7ns 878454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 881690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_8453719855824096461.key 881690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 881799 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15358603599931016610.key 881799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15358603599931016610.key 881799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.6ns 881799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 885303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15358603599931016610.key 885303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 885412 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2253386938034738211.key 885412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2253386938034738211.key 885412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.2ns 885412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 888994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2253386938034738211.key 888994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 889103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12906276368478291848.key 889103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12906276368478291848.key 889103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.5ns 889103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 892105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12906276368478291848.key 892105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 892215 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4485684412575498795.key 892215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4485684412575498795.key 892215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338ns 892215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 895264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4485684412575498795.key 895280 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 895389 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_5170358326468128676.key 895389 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_5170358326468128676.key 895389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 895389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 898406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5170358326468128676.key 898421 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.6ns 898531 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14334382974186162443.key 898531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14334382974186162443.key 898531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.5ns 898531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 901688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 901704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_14334382974186162443.key 901704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 901813 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_17520109847894207833.key 901813 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_17520109847894207833.key 901813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 655ns 901813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 904956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 904972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17520109847894207833.key 904972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 905084 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7932513874139174961.key 905084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7932513874139174961.key 905084 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.8ns 905084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 908383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 908399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7932513874139174961.key 908414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns