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.519s | 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.599s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.514s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.347s | 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.470s | 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.565s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.650s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.613s | 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.578s | 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.531s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.615s | 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.305s | 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.458s | 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.618s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.629s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.577s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.387s | 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.764s | 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] | 5.743s | 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.673s | 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.676s | 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.669s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.626s | 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.539s | 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.463s | passed |
Standard output
1253312 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 1253312 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 1253312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 1253312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1258775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 1258807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1258807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 1258922 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2165107220249575167.key 1258922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2165107220249575167.key 1258922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.2ns 1258922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1264555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 1264571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2165107220249575167.key 1264571 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1264686 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 1264686 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 1264686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 1264702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1270270 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 1270301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1270317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.27ms 1270430 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18117509327088791804.key 1270430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18117509327088791804.key 1270430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264ns 1270430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1275939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.51s 1275993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_18117509327088791804.key 1275993 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1276103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17156310233061201095.key 1276103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17156310233061201095.key 1276103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.8ns 1276103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1281651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 1281667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17156310233061201095.key 1281667 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1281780 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9708979610938964314.key 1281780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9708979610938964314.key 1281780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.8ns 1281780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1287308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1287339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9708979610938964314.key 1287340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1287449 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10716404966566665852.key 1287449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10716404966566665852.key 1287449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.1ns 1287449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1292949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 1292964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10716404966566665852.key 1292964 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52ns 1293075 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15471095696866030291.key 1293075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15471095696866030291.key 1293075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.2ns 1293075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1298474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1298489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15471095696866030291.key 1298505 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.6ns 1298614 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_3771760055130812780.key 1298614 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_3771760055130812780.key 1298614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.5ns 1298614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1303944 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 1303960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3771760055130812780.key 1303960 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 1304077 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4342320987686514810.key 1304077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4342320987686514810.key 1304077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.2ns 1304077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1309456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 1309487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4342320987686514810.key 1309487 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ns 1309596 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 1309596 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 1309596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.7ns 1309612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1315055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1315071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1315086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 1315196 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2068527783679920855.key 1315196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2068527783679920855.key 1315196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.2ns 1315196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1320565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 1320597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2068527783679920855.key 1320597 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1320710 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7701349276829897823.key 1320710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7701349276829897823.key 1320710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.5ns 1320710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1325916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1325932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7701349276829897823.key 1325947 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1326057 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17241614097997997758.key 1326057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17241614097997997758.key 1326057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279ns 1326057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1331402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 1331418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17241614097997997758.key 1331418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1331527 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13572833350576908211.key 1331527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13572833350576908211.key 1331527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.7ns 1331527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1336951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 1336982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13572833350576908211.key 1336982 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1337092 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_921554906752467228.key 1337092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_921554906752467228.key 1337092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.6ns 1337092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1342617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1342632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_921554906752467228.key 1342632 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 1342743 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16054881719391401969.key 1342743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16054881719391401969.key 1342743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269ns 1342743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1348215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 1348231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16054881719391401969.key 1348231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ns 1348356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7805020953543622004.key 1348356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7805020953543622004.key 1348356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.3ns 1348356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1353805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1353821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7805020953543622004.key 1353821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 1353934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10282428912298028656.key 1353934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10282428912298028656.key 1353934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.6ns 1353934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1359323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1359355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10282428912298028656.key 1359355 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 1359465 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5756053165953160321.key 1359465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5756053165953160321.key 1359465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.1ns 1359465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1364614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 1364630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5756053165953160321.key 1364630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1364771 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12551906341095514989.key 1364771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12551906341095514989.key 1364771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.9ns 1364771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1370088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 1370104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12551906341095514989.key 1370119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1370229 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_9123898267466352235.key 1370229 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_9123898267466352235.key 1370229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.9ns 1370229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1375706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1375737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_9123898267466352235.key 1375737 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23ns 1375847 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16495594891280083769.key 1375847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16495594891280083769.key 1375847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.9ns 1375847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1381336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1381351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16495594891280083769.key 1381351 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1381477 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_10793005681862655366.key 1381477 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_10793005681862655366.key 1381477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288ns 1381477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1386913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 1386929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10793005681862655366.key 1386929 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 1387054 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7855132347831761194.key 1387054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7855132347831761194.key 1387054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220ns 1387054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1392316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1392331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7855132347831761194.key 1392331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns