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.415s | 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.584s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.645s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.506s | 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.477s | 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.788s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.725s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.728s | 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.528s | 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.845s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.632s | 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.393s | 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.396s | 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.696s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.693s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.518s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.458s | 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.479s | 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.516s | 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.607s | 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.535s | 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.513s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.459s | 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.757s | 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.489s | passed |
Standard output
821369 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 821369 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 821369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.4ns 821384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 824887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 824887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 824998 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7623709101661905504.key 824998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7623709101661905504.key 824998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.5ns 824998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828347 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 828363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_7623709101661905504.key 828363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 828477 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 828477 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 828477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 828477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 831849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 831880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.69ms 831993 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_454579141596418756.key 831993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_454579141596418756.key 831993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.1ns 831993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 835485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_454579141596418756.key 835485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 835600 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10336304067681357332.key 835600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10336304067681357332.key 835600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 835600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839010 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 839026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10336304067681357332.key 839026 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 839136 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7491517548243293844.key 839136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7491517548243293844.key 839136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159ns 839136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 842524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7491517548243293844.key 842524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 842649 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8586254114163063329.key 842649 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8586254114163063329.key 842649 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.2ns 842649 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 845997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8586254114163063329.key 845997 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 846108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_8668438157812632788.key 846108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_8668438157812632788.key 846108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.6ns 846108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 849751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_8668438157812632788.key 849751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 849865 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_5691615522144213206.key 849865 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_5691615522144213206.key 849865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.3ns 849865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 853246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_5691615522144213206.key 853246 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 853355 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8857080361168315410.key 853355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8857080361168315410.key 853355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.8ns 853355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 856660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_8857080361168315410.key 856660 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 856770 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 856770 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 856770 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 856770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 860099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 860239 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 137.39ms 860354 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5673155711742892145.key 860354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5673155711742892145.key 860354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 860354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 863887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5673155711742892145.key 863887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 864000 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8849339770477759417.key 864000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8849339770477759417.key 864000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.9ns 864000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 867398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8849339770477759417.key 867398 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 867507 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_212079390716988984.key 867507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_212079390716988984.key 867507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.1ns 867507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 870869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_212079390716988984.key 870869 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 870984 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7865548696018848925.key 870984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7865548696018848925.key 870984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.5ns 870984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 874397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7865548696018848925.key 874397 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 874772 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6174664750602725480.key 874772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6174664750602725480.key 874788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.6ns 874788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 878358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6174664750602725480.key 878389 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 878498 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6145330733198111846.key 878498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6145330733198111846.key 878498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.96ms 878530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 882087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 882102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6145330733198111846.key 882102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 882227 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15051104196898787027.key 882227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15051104196898787027.key 882227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 882227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 885645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15051104196898787027.key 885645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 885801 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8919644215838942994.key 885801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8919644215838942994.key 885801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.9ns 885801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 889483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 889500 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8919644215838942994.key 889501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 889612 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6917763150359929970.key 889612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6917763150359929970.key 889612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 889612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 892896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6917763150359929970.key 892896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 893005 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7789083945113281583.key 893005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7789083945113281583.key 893005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.9ns 893005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 896272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 896287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7789083945113281583.key 896287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 896401 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_13368258849522912287.key 896401 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_13368258849522912287.key 896401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 564.9ns 896401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 899985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13368258849522912287.key 899985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 900098 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15473736798221532220.key 900098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15473736798221532220.key 900098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.3ns 900098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 903682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15473736798221532220.key 903682 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 903792 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_10070758879138795340.key 903792 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_10070758879138795340.key 903792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.9ns 903792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 907170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 907186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10070758879138795340.key 907186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 907311 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10598935618553025098.key 907311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10598935618553025098.key 907311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246ns 907311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 910594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 910641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_10598935618553025098.key 910641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns