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] | 3.367s | 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] | 3.275s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.324s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.284s | 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] | 3.487s | 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] | 3.418s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.377s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.270s | 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] | 3.239s | 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] | 3.264s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.396s | 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] | 3.382s | 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] | 3.367s | 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] | 3.301s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.143s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.124s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.219s | 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] | 3.359s | 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] | 3.365s | 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] | 3.226s | 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] | 3.175s | 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] | 3.253s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.275s | 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] | 3.455s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.312s | passed |
Standard output
809020 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 809020 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 809020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 809020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 812287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 812287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 812402 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12134543414858299137.key 812402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12134543414858299137.key 812402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.3ns 812402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 815648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_12134543414858299137.key 815649 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 815761 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 815761 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 815761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.6ns 815761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 818986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 819017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.09ms 819126 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7447697019699568969.key 819126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7447697019699568969.key 819126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.8ns 819126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 822237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7447697019699568969.key 822237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 822352 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9366786624321320259.key 822352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9366786624321320259.key 822352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.1ns 822352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 825417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9366786624321320259.key 825417 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 825527 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10585040491181371770.key 825527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10585040491181371770.key 825527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.3ns 825527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 828671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10585040491181371770.key 828671 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 828780 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16855479291281068535.key 828780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16855479291281068535.key 828780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.4ns 828780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 831941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16855479291281068535.key 831941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 832055 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14109531422016043215.key 832055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14109531422016043215.key 832055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.7ns 832055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 835399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_14109531422016043215.key 835399 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 835511 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_3320334303209249737.key 835511 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_3320334303209249737.key 835511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.2ns 835511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 838711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3320334303209249737.key 838711 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 838824 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13929427694461055001.key 838824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13929427694461055001.key 838824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.3ns 838824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 842082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13929427694461055001.key 842082 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 842191 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 842191 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 842191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.8ns 842191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 845341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 845356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 845466 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11443182910155333970.key 845466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11443182910155333970.key 845466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.4ns 845466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 848681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11443182910155333970.key 848681 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 848790 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4263299258873015578.key 848790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4263299258873015578.key 848790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.6ns 848790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 851948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 851964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4263299258873015578.key 851964 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 852074 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1323984881549667650.key 852074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1323984881549667650.key 852074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.8ns 852074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 855451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_1323984881549667650.key 855451 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ns 855561 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8586170971375897669.key 855561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8586170971375897669.key 855593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 855593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 858863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8586170971375897669.key 858863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 858979 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12827236306587837513.key 858979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12827236306587837513.key 858979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.7ns 858979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 862248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12827236306587837513.key 862248 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 862357 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15146933856444565466.key 862357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15146933856444565466.key 862357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.8ns 862357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 865514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15146933856444565466.key 865514 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 865627 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15348481484998635262.key 865627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15348481484998635262.key 865627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.2ns 865627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 868739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 868755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15348481484998635262.key 868755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 868866 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_975604927413171162.key 868866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_975604927413171162.key 868866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns 868866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 872015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_975604927413171162.key 872015 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 872130 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13839291798762628014.key 872130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13839291798762628014.key 872130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.65ms 872130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 875381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 875397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13839291798762628014.key 875397 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.8ns 875512 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17546082783916033685.key 875512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17546082783916033685.key 875512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 875512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878758 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 878774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17546082783916033685.key 878774 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 878879 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_8521128555951985510.key 878879 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_8521128555951985510.key 878879 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.3ns 878879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 882056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 882072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8521128555951985510.key 882072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 882181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8971346904157979437.key 882181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8971346904157979437.key 882181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.2ns 882181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 885214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8971346904157979437.key 885214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 885324 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_13387256148027955307.key 885324 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_13387256148027955307.key 885324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277ns 885324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 888334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13387256148027955307.key 888334 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 888448 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7540946817802538779.key 888448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7540946817802538779.key 888448 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.6ns 888448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 891542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7540946817802538779.key 891558 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ns