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.331s | 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.409s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.314s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.315s | 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.471s | 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.300s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.376s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.520s | 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.363s | 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.268s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.675s | 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.425s | 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.379s | 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.393s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.442s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.285s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.348s | 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.564s | 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.567s | 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.612s | 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.486s | 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.362s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.425s | 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.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] | 4.408s | passed |
Standard output
1006614 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 1006614 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 1006614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 1006614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1011148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 1011164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1011180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 1011289 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14695653042621005151.key 1011289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14695653042621005151.key 1011289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.1ns 1011289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1015713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 1015728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14695653042621005151.key 1015728 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1015853 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 1015853 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 1015853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 1015853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1020264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 1020279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1020310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.9ms 1020420 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17115207815224728167.key 1020420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17115207815224728167.key 1020420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.8ns 1020420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1024891 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 1024907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17115207815224728167.key 1024922 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1025032 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16747897227853525299.key 1025032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16747897227853525299.key 1025032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.2ns 1025032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1029409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16747897227853525299.key 1029409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1029518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7217693475033050952.key 1029518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7217693475033050952.key 1029518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.9ns 1029518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1033770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7217693475033050952.key 1033770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1033880 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4903894185916025324.key 1033880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4903894185916025324.key 1033880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.6ns 1033880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1038195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_4903894185916025324.key 1038195 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1038305 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17969957019920099339.key 1038305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17969957019920099339.key 1038305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.5ns 1038305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1042683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17969957019920099339.key 1042683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1042792 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_12716820061632978803.key 1042792 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_12716820061632978803.key 1042792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.7ns 1042792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1047091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12716820061632978803.key 1047091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 1047201 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11105284733630338492.key 1047201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11105284733630338492.key 1047201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.3ns 1047201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1051423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11105284733630338492.key 1051423 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1051533 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 1051533 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 1051533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.8ns 1051533 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1055832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1055832 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 1055942 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11323396689545021137.key 1055942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11323396689545021137.key 1055942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.3ns 1055942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1060147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11323396689545021137.key 1060147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 1060256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13435868911455335052.key 1060256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13435868911455335052.key 1060256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.9ns 1060256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1064446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13435868911455335052.key 1064446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1064571 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17081078501409468198.key 1064571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17081078501409468198.key 1064571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.1ns 1064571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1068917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1068933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17081078501409468198.key 1068933 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1069042 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11331877570002339556.key 1069042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11331877570002339556.key 1069042 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.6ns 1069042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1073217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1073233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11331877570002339556.key 1073233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1073342 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13846409981741977913.key 1073342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13846409981741977913.key 1073342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 446ns 1073342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1077595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1077610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13846409981741977913.key 1077610 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1077719 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10844152356325032618.key 1077719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10844152356325032618.key 1077719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.9ns 1077719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1082114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s 1082129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_10844152356325032618.key 1082129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1082239 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1623384755434554679.key 1082239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1623384755434554679.key 1082239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 1082239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1086477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1086493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1623384755434554679.key 1086493 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1086602 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15526795929407526458.key 1086602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15526795929407526458.key 1086602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns 1086602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1090745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1090761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15526795929407526458.key 1090761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1090870 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7733468704881734246.key 1090870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7733468704881734246.key 1090870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 1090870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1095170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1095186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7733468704881734246.key 1095186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1095295 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14253473964365881358.key 1095295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14253473964365881358.key 1095295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.6ns 1095295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1099549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1099564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14253473964365881358.key 1099564 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1099674 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_1931552717709925780.key 1099674 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_1931552717709925780.key 1099674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.5ns 1099674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1103926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1103957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1931552717709925780.key 1103957 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1104067 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18265758940493444773.key 1104067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18265758940493444773.key 1104067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 1104067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1108353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1108400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_18265758940493444773.key 1108400 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1108509 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_458747723518898721.key 1108509 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_458747723518898721.key 1108509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.6ns 1108509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1112654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1112685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_458747723518898721.key 1112685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1112794 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18189623064480236748.key 1112794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18189623064480236748.key 1112794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.7ns 1112794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1117001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 1117033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18189623064480236748.key 1117033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns