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.684s | 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.426s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.480s | 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.621s | 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.535s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.524s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.566s | 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.476s | 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] | 6.237s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 6.017s | 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.550s | 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.584s | 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.598s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.502s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.598s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.688s | 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.640s | 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.114s | 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.475s | 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.753s | 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.587s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.585s | 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.373s | 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.657s | passed |
Standard output
1271050 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 1271050 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 1271050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 1271050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1276923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.87s 1276939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1276955 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 1277064 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17909348494379344283.key 1277064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17909348494379344283.key 1277064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.9ns 1277080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1282551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1282582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17909348494379344283.key 1282582 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 1282706 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 1282706 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 1282706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.6ns 1282722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.9s 1288648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1288711 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.62ms 1288820 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3799909659025960716.key 1288820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3799909659025960716.key 1288820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 1288820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 1294183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3799909659025960716.key 1294183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ns 1294295 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17157523207582388716.key 1294295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17157523207582388716.key 1294295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.2ns 1294295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s 1299939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17157523207582388716.key 1299939 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1300048 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9781169814057413620.key 1300048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9781169814057413620.key 1300048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 1300048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1305510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1305526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9781169814057413620.key 1305526 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 1305636 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16418827611781049121.key 1305636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16418827611781049121.key 1305636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.8ns 1305636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1311092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1311108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16418827611781049121.key 1311108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1311221 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7474432842447530825.key 1311221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7474432842447530825.key 1311221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.3ns 1311221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1316464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.24s 1316479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7474432842447530825.key 1316479 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1316594 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_10201664960672518674.key 1316594 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_10201664960672518674.key 1316594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.8ns 1316594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1322119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1322134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10201664960672518674.key 1322134 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1322251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5506177460660839545.key 1322251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5506177460660839545.key 1322251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.7ns 1322251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1327790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 1327821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5506177460660839545.key 1327821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1327936 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 1327936 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 1327936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 1327936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1333343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 1333359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1333359 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 1333484 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12838174850415698184.key 1333484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12838174850415698184.key 1333484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.7ns 1333484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1338769 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1338785 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12838174850415698184.key 1338785 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1338910 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16892459146006345070.key 1338910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16892459146006345070.key 1338910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 1338910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1344262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 1344278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_16892459146006345070.key 1344278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1344390 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_462708896653671514.key 1344390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_462708896653671514.key 1344390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 579.2ns 1344390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1349886 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 1349902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_462708896653671514.key 1349902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1350012 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13014159611149396299.key 1350012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13014159611149396299.key 1350012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 1350012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1355406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1355437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13014159611149396299.key 1355437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1355547 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10016118853151195348.key 1355547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10016118853151195348.key 1355547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.3ms 1355547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1360932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 1360963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10016118853151195348.key 1360963 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1361073 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7170112924071991409.key 1361073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7170112924071991409.key 1361073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.4ns 1361073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1366498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 1366515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7170112924071991409.key 1366530 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1366639 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2235460187723014095.key 1366639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2235460187723014095.key 1366639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.6ns 1366639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1371971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 1372002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2235460187723014095.key 1372002 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1372115 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_12118188612214656791.key 1372115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_12118188612214656791.key 1372115 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.6ns 1372115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1378212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.1s 1378228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_12118188612214656791.key 1378228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1378353 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1015627527605877061.key 1378353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1015627527605877061.key 1378353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 594.3ns 1378353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1383763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 1383794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1015627527605877061.key 1383794 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1383904 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_483616323456190683.key 1383904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_483616323456190683.key 1383904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.6ns 1383904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1389360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1389376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_483616323456190683.key 1389376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1389488 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_9597842403738321543.key 1389488 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_9597842403738321543.key 1389488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.1ns 1389488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1394956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1394971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_9597842403738321543.key 1394971 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1395087 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17742789511261908378.key 1395087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17742789511261908378.key 1395087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.8ns 1395087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1400458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 1400473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17742789511261908378.key 1400473 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1400604 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_2362515572981715711.key 1400604 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_2362515572981715711.key 1400604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 704.8ns 1400604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1406065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1406080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_2362515572981715711.key 1406080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1406191 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3295337400563408585.key 1406191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3295337400563408585.key 1406191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.67ms 1406191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1411753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 1411769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3295337400563408585.key 1411769 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns