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.266s | 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.330s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.329s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.486s | 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.237s | 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.297s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.204s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.245s | 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.205s | 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.203s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.337s | 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.236s | 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.220s | 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.220s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.268s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.205s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.220s | 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.422s | 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.377s | 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.423s | 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.282s | 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.298s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.392s | 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.266s | 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.329s | passed |
Standard output
698125 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 698125 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 698125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 698125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 701330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 701345 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.06ms 701455 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15536633091416098505.key 701455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15536633091416098505.key 701455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.5ns 701455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 704769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15536633091416098505.key 704769 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 704878 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 704878 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 704878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.9ns 704878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708084 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 708099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 708146 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.41ms 708256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3679051310445764416.key 708256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3679051310445764416.key 708256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.7ns 708256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 711554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 711570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3679051310445764416.key 711570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 711680 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12914246126374542765.key 711680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12914246126374542765.key 711680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.1ns 711680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 714822 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 714838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12914246126374542765.key 714838 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 714963 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_6566573852710839326.key 714963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_6566573852710839326.key 714963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 714963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 718136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 718152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_6566573852710839326.key 718152 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 718261 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6307942170533755176.key 718261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6307942170533755176.key 718261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 581.1ns 718261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 721513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 721528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6307942170533755176.key 721544 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 721654 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_8001462452719263414.key 721654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_8001462452719263414.key 721654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.5ns 721654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 724796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 724812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_8001462452719263414.key 724812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 724921 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_11199398607634245283.key 724921 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_11199398607634245283.key 724921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.3ns 724921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 728126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 728141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11199398607634245283.key 728141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 728251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12356941995580262558.key 728251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12356941995580262558.key 728251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.2ns 728251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 731393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 731409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_12356941995580262558.key 731409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 731518 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 731518 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 731518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.7ns 731518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 734708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 734723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 734723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 734849 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7550182589338714508.key 734849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7550182589338714508.key 734849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 578.8ns 734849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 738038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 738053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7550182589338714508.key 738053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 738179 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5126890394364060168.key 738179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5126890394364060168.key 738179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.1ns 738179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 741494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 741510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5126890394364060168.key 741557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 741666 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_18151054963732511332.key 741666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_18151054963732511332.key 741666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.5ns 741666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 744778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 744793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_18151054963732511332.key 744793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 744903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12566847676464379890.key 744903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12566847676464379890.key 744903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 744903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 748045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 748061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12566847676464379890.key 748061 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 748217 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1713891288135578562.key 748217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1713891288135578562.key 748217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.5ns 748217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 751281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 751297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_1713891288135578562.key 751297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 751406 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2526867315660293575.key 751406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2526867315660293575.key 751422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.2ns 751422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 754534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 754549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2526867315660293575.key 754549 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 754659 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13588446193342712915.key 754659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13588446193342712915.key 754659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.3ns 754659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 757738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 757754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13588446193342712915.key 757754 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 757864 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14992164002795574500.key 757864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14992164002795574500.key 757864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.4ns 757864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 760927 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 760943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14992164002795574500.key 760943 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 761068 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14191572132486786414.key 761068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14191572132486786414.key 761068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.8ns 761068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 764180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 764196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14191572132486786414.key 764196 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 764304 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15316128076959381193.key 764304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15316128076959381193.key 764304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.5ns 764304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 767415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_15316128076959381193.key 767415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 767524 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_17716266414716918958.key 767524 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_17716266414716918958.key 767524 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.3ns 767524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 770620 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 770636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17716266414716918958.key 770636 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 770745 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_960190292954257419.key 770745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_960190292954257419.key 770745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.3ns 770745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 773889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 773905 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_960190292954257419.key 773905 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 774014 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_3505187753702202894.key 774014 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_3505187753702202894.key 774014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns 774014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 777094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 777109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3505187753702202894.key 777109 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 777219 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3047396372471857982.key 777219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3047396372471857982.key 777219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 777219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 780330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3047396372471857982.key 780330 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns