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.289s | 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.229s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.232s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.234s | 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] | 4.222s | 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.237s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.220s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.230s | 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] | 4.214s | 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.251s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.431s | 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] | 4.232s | 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] | 4.309s | 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] | 4.296s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.248s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.251s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.217s | 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] | 4.674s | 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] | 4.273s | 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] | 4.233s | 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] | 4.224s | 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] | 4.293s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.277s | 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] | 4.290s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.282s | passed |
Standard output
967517 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 967517 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 967517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 967533 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 971824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 971843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 971849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 971958 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11379446894356980302.key 971958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11379446894356980302.key 971958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332ns 971958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 976492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 976508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11379446894356980302.key 976524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 976633 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 976633 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 976633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 976633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 980734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 980781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 980796 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 980906 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3144932837432853804.key 980906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3144932837432853804.key 980906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.7ns 980906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 984998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 985014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3144932837432853804.key 985029 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 985139 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11460252265858581161.key 985139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11460252265858581161.key 985139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.7ns 985139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 989248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11460252265858581161.key 989248 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 989363 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14954643862240208114.key 989363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14954643862240208114.key 989363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257ns 989363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 993540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14954643862240208114.key 993540 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 993656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7208778143494683705.key 993656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7208778143494683705.key 993656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.7ns 993656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 997819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_7208778143494683705.key 997819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.9ns 997933 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3789282841470804396.key 997933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3789282841470804396.key 997933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.5ns 997933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1002098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3789282841470804396.key 1002098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1002223 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_12707800739192019824.key 1002223 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_12707800739192019824.key 1002223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 1002223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1006380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1006396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12707800739192019824.key 1006396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1006505 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16342170055879311547.key 1006505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16342170055879311547.key 1006505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.72ms 1006521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1010664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1010680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_16342170055879311547.key 1010680 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1010795 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 1010795 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 1010795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.9ns 1010795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1014892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1014908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1014908 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.4ns 1015024 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15659810780466950051.key 1015024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15659810780466950051.key 1015024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.9ns 1015024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1019124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1019139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15659810780466950051.key 1019139 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1019256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5599528732171809785.key 1019256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5599528732171809785.key 1019256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.9ns 1019256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1023364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1023380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5599528732171809785.key 1023380 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1023490 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3323481925981835264.key 1023490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3323481925981835264.key 1023490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.3ns 1023490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1027584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1027600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_3323481925981835264.key 1027600 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1027712 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9471096996720306418.key 1027712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9471096996720306418.key 1027712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.4ns 1027712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1031817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 1031833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9471096996720306418.key 1031833 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1031949 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11413898527252228702.key 1031949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11413898527252228702.key 1031949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.6ns 1031949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1036045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1036061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_11413898527252228702.key 1036061 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1036170 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4781697353955271333.key 1036170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4781697353955271333.key 1036170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251ns 1036170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1040272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1040288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4781697353955271333.key 1040288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1040400 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12603197442850861912.key 1040400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12603197442850861912.key 1040400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 1040400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1044489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 1044505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_12603197442850861912.key 1044505 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1044614 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15290546894656779173.key 1044614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15290546894656779173.key 1044614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.9ns 1044614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1048723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1048755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15290546894656779173.key 1048755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1048865 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5777531271015306672.key 1048865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5777531271015306672.key 1048865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.4ns 1048865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1052988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5777531271015306672.key 1052988 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1053097 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5331233849210280575.key 1053097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5331233849210280575.key 1053097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.5ns 1053097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1057265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1057296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5331233849210280575.key 1057296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 1057406 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_2214785048604267371.key 1057406 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_2214785048604267371.key 1057406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.5ns 1057406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1061541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1061556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2214785048604267371.key 1061587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1061702 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5038544766202722350.key 1061702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5038544766202722350.key 1061702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.1ns 1061702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1065825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1065840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5038544766202722350.key 1065840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1065950 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_17323888445926109837.key 1065950 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_17323888445926109837.key 1065950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.6ns 1065950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1070077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1070093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17323888445926109837.key 1070093 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1070202 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1060951869846370208.key 1070202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1060951869846370208.key 1070202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.5ns 1070202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1074288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1074303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1060951869846370208.key 1074303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns