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.596s | 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.517s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.533s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.772s | 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.676s | 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] | 5.103s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.114s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.989s | 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.818s | 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.912s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.571s | 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] | 5.034s | 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.788s | 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.800s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.454s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.471s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.579s | 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.565s | 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.814s | 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.502s | 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.642s | 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.519s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.658s | 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.580s | 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.564s | passed |
Standard output
810572 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 810572 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 810572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 810587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 814011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 814026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 814042 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 814151 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13185446166940480398.key 814151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13185446166940480398.key 814151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.8ns 814151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 817606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13185446166940480398.key 817606 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 817716 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 817870 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 817870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 593.7ns 817872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 821390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 821406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.23ms 821531 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_219786674376673874.key 821531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_219786674376673874.key 821531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 821531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 824923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_219786674376673874.key 824923 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 825033 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3823939567944183511.key 825033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3823939567944183511.key 825033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.1ns 825033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 828566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3823939567944183511.key 828566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 828675 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2932691760596001655.key 828675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2932691760596001655.key 828675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.5ns 828675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 832069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2932691760596001655.key 832085 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 832194 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_233677807553313333.key 832194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_233677807553313333.key 832194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.3ns 832194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 835727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_233677807553313333.key 835743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 835852 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3672851512602971624.key 835852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3672851512602971624.key 835852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182ns 835852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839307 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 839323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3672851512602971624.key 839323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 839432 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_6682673353810285683.key 839432 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_6682673353810285683.key 839432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.6ns 839432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 842887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_6682673353810285683.key 842887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 842997 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2779092032702720823.key 842997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2779092032702720823.key 842997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.2ns 842997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 846467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 846483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_2779092032702720823.key 846483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 846593 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 846593 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 846593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.8ns 846593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 850000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 850000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 850110 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11850820469741546175.key 850110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11850820469741546175.key 850110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.9ns 850110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 853534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11850820469741546175.key 853534 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 853644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15359875691078053484.key 853644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15359875691078053484.key 853644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.3ns 853644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 858291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15359875691078053484.key 858291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ns 858479 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12144267339108077448.key 858495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12144267339108077448.key 858495 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.26ms 858510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 862986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12144267339108077448.key 862986 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 863174 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11729912392866262487.key 863191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11729912392866262487.key 863191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.86ms 863254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 868102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 868117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11729912392866262487.key 868117 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 868227 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_531130687717760003.key 868227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_531130687717760003.key 868227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244ns 868227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 873059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 873075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_531130687717760003.key 873106 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 873357 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6714498601197630981.key 873357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6714498601197630981.key 873357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178ns 873357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 878223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6714498601197630981.key 878223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 878332 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17194793624338240063.key 878332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17194793624338240063.key 878332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns 878332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 882978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 883041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17194793624338240063.key 883041 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 883150 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_451629710242403966.key 883150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_451629710242403966.key 883150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.8ns 883150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 887936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_451629710242403966.key 887936 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 888124 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12944024334694784625.key 888156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12944024334694784625.key 888171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.73ms 888218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 893009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12944024334694784625.key 893009 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 893118 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8612884219503992926.key 893118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8612884219503992926.key 893118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.1ns 893118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 897766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 897781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8612884219503992926.key 897797 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 897906 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_6471687911237970184.key 897906 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_6471687911237970184.key 897906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 897906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 902598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6471687911237970184.key 902598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 902707 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12671885019198511089.key 902707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12671885019198511089.key 902707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.7ns 902707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 906053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12671885019198511089.key 906053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 906162 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_4288724865860519248.key 906162 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_4288724865860519248.key 906162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.2ns 906162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 909524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4288724865860519248.key 909524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 909634 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9536726614355978791.key 909634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9536726614355978791.key 909634 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.3ns 909634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 913105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9536726614355978791.key 913105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns