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] | 5.534s | 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] | 5.547s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.655s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.508s | 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] | 5.432s | 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.322s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.180s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.332s | 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] | 5.237s | 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] | 5.552s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.424s | 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.275s | 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] | 5.321s | 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] | 5.286s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.295s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.357s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.418s | 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] | 5.628s | 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] | 6.164s | 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] | 5.366s | 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] | 5.440s | 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] | 5.442s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.431s | 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] | 5.425s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 5.429s | passed |
Standard output
1221719 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 1221719 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 1221719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 1221719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1227006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1227022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1227037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 1227147 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8214464390724389603.key 1227147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8214464390724389603.key 1227147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.8ns 1227147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1232635 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 1232650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8214464390724389603.key 1232666 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1232775 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 1232775 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 1232775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.5ns 1232775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1238780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6s 1238796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1238827 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.77ms 1238940 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7276328672917502778.key 1238940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7276328672917502778.key 1238940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.1ns 1238940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1244165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 1244197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7276328672917502778.key 1244197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1244306 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17185973973324070969.key 1244306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17185973973324070969.key 1244306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 618.7ns 1244306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1249615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1249631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17185973973324070969.key 1249631 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1249746 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8661737145867281460.key 1249746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8661737145867281460.key 1249746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.2ns 1249746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1255048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1255063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8661737145867281460.key 1255063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1255188 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5446087761038007136.key 1255188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5446087761038007136.key 1255188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.9ns 1255188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1260488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1260503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5446087761038007136.key 1260503 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.3ns 1260619 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10888394986731764432.key 1260619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10888394986731764432.key 1260619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288ns 1260619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1265903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1265935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10888394986731764432.key 1265935 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1266044 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_5915694032857032476.key 1266044 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_5915694032857032476.key 1266044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.4ns 1266044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1271332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1271348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_5915694032857032476.key 1271348 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 1271473 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3468081139526764398.key 1271473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3468081139526764398.key 1271473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.7ns 1271489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1276880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1276896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3468081139526764398.key 1276896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1277008 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 1277008 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 1277008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.6ns 1277008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1282415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 1282446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1282446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 1282555 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17905024502736349718.key 1282555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17905024502736349718.key 1282555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.4ns 1282555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1288098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17905024502736349718.key 1288098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1288210 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9927416261940989425.key 1288210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9927416261940989425.key 1288210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.8ns 1288210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1293576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 1293608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9927416261940989425.key 1293608 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1293718 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5248819630572137169.key 1293718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5248819630572137169.key 1293718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.1ns 1293718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1299034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5248819630572137169.key 1299034 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ns 1299150 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10698721776584656263.key 1299150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10698721776584656263.key 1299150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.1ns 1299150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.19s 1304347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10698721776584656263.key 1304363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1304472 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17576711137033633803.key 1304472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17576711137033633803.key 1304472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 595ns 1304472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1309521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 1309537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_17576711137033633803.key 1309537 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1309653 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11077289095524938593.key 1309653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11077289095524938593.key 1309653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.5ns 1309653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1314860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1314876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11077289095524938593.key 1314876 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1314986 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15915844809596992267.key 1314986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15915844809596992267.key 1314986 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns 1314986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1320098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1320114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15915844809596992267.key 1320114 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns 1320223 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8651092646464889843.key 1320223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8651092646464889843.key 1320223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.1ns 1320223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1325588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 1325619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8651092646464889843.key 1325635 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1325792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_10768386112752771659.key 1325792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_10768386112752771659.key 1325792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 465ns 1325792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1330926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 1330942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_10768386112752771659.key 1330942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.7ns 1331051 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4781920110441914102.key 1331051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4781920110441914102.key 1331051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.2ns 1331051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1336241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1336256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4781920110441914102.key 1336256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1336372 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_12417322888168845109.key 1336372 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_12417322888168845109.key 1336372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.4ns 1336372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1341531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 1341547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12417322888168845109.key 1341547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1341674 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12962037544446522595.key 1341674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12962037544446522595.key 1341674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.7ns 1341689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1346815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 1346831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12962037544446522595.key 1346847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1346956 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_2822270457706170167.key 1346956 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_2822270457706170167.key 1346956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.5ns 1346956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1352190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 1352205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_2822270457706170167.key 1352205 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1352315 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5213633652286442233.key 1352315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5213633652286442233.key 1352315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.7ns 1352315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1357603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1357618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5213633652286442233.key 1357618 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns