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.239s | 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.297s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.297s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.260s | 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.294s | 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.317s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.360s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.353s | 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.312s | 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.383s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.314s | 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.342s | 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.318s | 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.304s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.295s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.272s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.319s | 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.317s | 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.282s | 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.258s | 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.255s | 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.287s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.280s | 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.255s | 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.264s | passed |
Standard output
984711 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 984711 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 984711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 984711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 988873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 988889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 988904 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 989014 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16446164202761059342.key 989014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16446164202761059342.key 989014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.5ns 989014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 993216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16446164202761059342.key 993216 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 993331 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 993331 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 993331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.6ns 993331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997457 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 997473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 997504 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.41ms 997613 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10963702316124132812.key 997613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10963702316124132812.key 997613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.2ns 997613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1001727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 1001762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_10963702316124132812.key 1001762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1001871 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12832533300830956623.key 1001871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12832533300830956623.key 1001871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 1001871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1005993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1006008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12832533300830956623.key 1006008 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1006126 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15433132312581203035.key 1006126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15433132312581203035.key 1006126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 1006126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1010287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1010302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15433132312581203035.key 1010302 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1010413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4425904262067125330.key 1010413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4425904262067125330.key 1010413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.8ns 1010413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1014552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1014584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_4425904262067125330.key 1014584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.5ns 1014693 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18034390276454649293.key 1014693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18034390276454649293.key 1014693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.2ns 1014693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1018807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1018822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_18034390276454649293.key 1018838 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1018948 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_4038612246505317279.key 1018948 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_4038612246505317279.key 1018948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.7ns 1018948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1023081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1023097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4038612246505317279.key 1023097 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1023212 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5801630641356321195.key 1023212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5801630641356321195.key 1023212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.4ns 1023212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1027327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 1027343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5801630641356321195.key 1027343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1027452 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 1027452 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 1027452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.2ns 1027452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1031608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1031623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1031639 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 1031749 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8471501342636142800.key 1031749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8471501342636142800.key 1031749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.4ns 1031749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1035905 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1035936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8471501342636142800.key 1035936 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1036046 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14086235447747641494.key 1036046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14086235447747641494.key 1036046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 1036046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1040164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1040180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14086235447747641494.key 1040180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1040306 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9423753348773559535.key 1040306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9423753348773559535.key 1040306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.2ns 1040306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1044468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1044484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9423753348773559535.key 1044484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1044600 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1209773679779081855.key 1044600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1209773679779081855.key 1044600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 1044600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1048785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1048801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_1209773679779081855.key 1048801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1048917 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11683584906362450979.key 1048917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11683584906362450979.key 1048917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.77ms 1048917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1053138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1053153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_11683584906362450979.key 1053153 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1053278 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13387187650724335468.key 1053278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13387187650724335468.key 1053278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262ns 1053278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1057501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1057516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13387187650724335468.key 1057516 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1057631 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7900123103981350113.key 1057631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7900123103981350113.key 1057631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.5ns 1057631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1061818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1061833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7900123103981350113.key 1061833 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1061943 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2547837939530864847.key 1061943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2547837939530864847.key 1061943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.9ns 1061943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1066200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1066216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2547837939530864847.key 1066216 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1066326 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6225995933296518268.key 1066326 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6225995933296518268.key 1066326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.8ns 1066326 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1070538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 1070553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6225995933296518268.key 1070553 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1070668 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_18092107568027473265.key 1070668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_18092107568027473265.key 1070668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.5ns 1070668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1074854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1074869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_18092107568027473265.key 1074869 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ns 1074986 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_5256718079462808635.key 1074986 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_5256718079462808635.key 1074986 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.9ns 1074986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1079165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1079165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5256718079462808635.key 1079181 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1079290 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_13472776235013810015.key 1079290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_13472776235013810015.key 1079290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.7ns 1079290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1083444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1083460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_13472776235013810015.key 1083460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1083585 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_1257708253077620051.key 1083585 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_1257708253077620051.key 1083585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 1083585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1087728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1087743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1257708253077620051.key 1087743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1087857 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12796774483574445975.key 1087857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12796774483574445975.key 1087857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.9ns 1087857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1092051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1092066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12796774483574445975.key 1092066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns