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.224s | 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.194s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.187s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.201s | 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.204s | 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.175s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.180s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.186s | 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.186s | 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.157s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.346s | 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.177s | 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.218s | 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.156s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.168s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.195s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.162s | 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.233s | 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.281s | 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.218s | 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.190s | 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.220s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.226s | 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.239s | 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.201s | passed |
Standard output
959292 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 959292 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 959292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 959307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 963493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 963509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 963525 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 963634 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7063181589584392055.key 963634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7063181589584392055.key 963634 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.5ns 963634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 967735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 967750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_7063181589584392055.key 967750 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 967867 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 967867 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 967867 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.2ns 967867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 972001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 972017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 972032 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 972148 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_182108376409771846.key 972148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_182108376409771846.key 972148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 972148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 976241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 976256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_182108376409771846.key 976256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 976366 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12698784067902475582.key 976366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12698784067902475582.key 976366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126ns 976366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 980429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 980445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12698784067902475582.key 980445 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 980556 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12522034563908013095.key 980556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12522034563908013095.key 980556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 980556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 984647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 984663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12522034563908013095.key 984663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 984776 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17929252010895590671.key 984776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17929252010895590671.key 984776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.2ns 984776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 988875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 988890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17929252010895590671.key 988890 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.9ns 989002 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4359684540925470670.key 989002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4359684540925470670.key 989002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.8ns 989002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 993128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4359684540925470670.key 993128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 993241 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_12431900336890299813.key 993241 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_12431900336890299813.key 993241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.3ns 993241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997313 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 997329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12431900336890299813.key 997329 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 997442 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5823573765160976655.key 997442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5823573765160976655.key 997442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.1ns 997442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1001526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1001541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5823573765160976655.key 1001557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1001667 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 1001667 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 1001667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.9ns 1001667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1005731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1005747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1005747 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 1005861 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3784493885491316674.key 1005861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3784493885491316674.key 1005861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.1ns 1005861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1009923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1009939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3784493885491316674.key 1009939 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1010048 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_18347872796550388039.key 1010048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_18347872796550388039.key 1010048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.6ns 1010048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1014120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1014136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_18347872796550388039.key 1014136 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1014249 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10059415958868365618.key 1014249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10059415958868365618.key 1014249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.1ns 1014249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1018331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 1018347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10059415958868365618.key 1018347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1018453 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12820517590510954205.key 1018453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12820517590510954205.key 1018453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 1018453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1022487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1022503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12820517590510954205.key 1022518 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1022628 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17255455023646571836.key 1022628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17255455023646571836.key 1022628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.4ns 1022628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1026680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1026696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_17255455023646571836.key 1026696 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1026809 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3564484200612535628.key 1026809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3564484200612535628.key 1026809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.7ns 1026809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1030869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1030885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3564484200612535628.key 1030885 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1030995 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10410328286084655069.key 1030995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10410328286084655069.key 1030995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 1030995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1035050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1035066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10410328286084655069.key 1035066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1035181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2690899624857129966.key 1035181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2690899624857129966.key 1035181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 1035181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1039218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 1039233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2690899624857129966.key 1039233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1039338 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15708431418303133436.key 1039338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15708431418303133436.key 1039338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.6ns 1039338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1043383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1043399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15708431418303133436.key 1043399 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1043515 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2148790489028224322.key 1043515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2148790489028224322.key 1043515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 1043515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1047624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2148790489028224322.key 1047624 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1047733 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_1560205773628137226.key 1047733 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_1560205773628137226.key 1047733 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.8ns 1047733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 1051780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1560205773628137226.key 1051780 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1051890 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8786634874807146065.key 1051890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8786634874807146065.key 1051890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns 1051890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1055948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8786634874807146065.key 1055948 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1056073 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_15781292837232935923.key 1056073 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_15781292837232935923.key 1056073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.5ns 1056073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1060164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15781292837232935923.key 1060164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1060274 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8984879186593650023.key 1060274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8984879186593650023.key 1060274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 1060274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1064327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8984879186593650023.key 1064327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns