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.299s | 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.520s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.295s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.318s | 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.338s | 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.337s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.333s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.424s | 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.719s | 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.400s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.918s | 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.410s | 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.336s | 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.378s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.479s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.115s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.484s | 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.347s | 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.419s | 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.555s | 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.720s | 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.441s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.573s | 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.339s | 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.322s | passed |
Standard output
791409 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 791409 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 791409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 791456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 795207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 795207 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 795332 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_623128071021403933.key 795332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_623128071021403933.key 795332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.5ns 795332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 798569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_623128071021403933.key 798569 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 798679 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 798679 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 798679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.4ns 798679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 801953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 801985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.44ms 802098 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10170471401109209501.key 802098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10170471401109209501.key 802098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.6ns 802098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 805538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_10170471401109209501.key 805538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 805653 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14477373283231753129.key 805653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14477373283231753129.key 805653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.7ns 805653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 809249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14477373283231753129.key 809249 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 809374 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15067838787025532244.key 809374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15067838787025532244.key 809374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.7ns 809374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 812705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15067838787025532244.key 812705 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 812815 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2629210173403709859.key 812815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2629210173403709859.key 812815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.4ns 812815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 816280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2629210173403709859.key 816280 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 816389 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5419409974801823227.key 816389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5419409974801823227.key 816389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.9ns 816389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 819619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5419409974801823227.key 819619 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 819728 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_251014756360147506.key 819728 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_251014756360147506.key 819728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.4ns 819728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 822940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_251014756360147506.key 822940 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 823050 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_17110841712088314557.key 823050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_17110841712088314557.key 823050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279ns 823050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 826208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 826223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_17110841712088314557.key 826223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 826349 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 826349 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 826349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 826353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 829635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 829760 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.94ms 829869 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11321958569731218985.key 829869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11321958569731218985.key 829869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.3ns 829869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 833052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11321958569731218985.key 833052 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 833165 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7551802968829844288.key 833165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7551802968829844288.key 833165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.2ns 833165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 836354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 836370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7551802968829844288.key 836370 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 836483 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11141434705074740957.key 836483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11141434705074740957.key 836483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.9ns 836483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 839706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11141434705074740957.key 839706 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 839821 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15346180602394228309.key 839821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15346180602394228309.key 839821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.7ns 839821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 843034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 843050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15346180602394228309.key 843050 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 843159 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4321535137121032612.key 843159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4321535137121032612.key 843159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.8ns 843159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 846366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 846382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4321535137121032612.key 846382 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 846492 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12980015616912010804.key 846492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12980015616912010804.key 846492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.5ns 846492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 849759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12980015616912010804.key 849759 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 849916 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2675226160172782198.key 849916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2675226160172782198.key 849916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.2ns 849916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 853511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2675226160172782198.key 853511 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 853636 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6428479572993485833.key 853636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6428479572993485833.key 853636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 853636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 856925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6428479572993485833.key 856925 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 857036 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11794038973860468689.key 857036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11794038973860468689.key 857036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.8ns 857036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 860337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11794038973860468689.key 860337 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 860446 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9868255023369315568.key 860446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9868255023369315568.key 860446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 860446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 863657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9868255023369315568.key 863657 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 863782 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_17827520695033426233.key 863782 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_17827520695033426233.key 863782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.2ns 863782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 867035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17827520695033426233.key 867050 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 867160 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5470477502944600926.key 867160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5470477502944600926.key 867160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.2ns 867160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 870529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5470477502944600926.key 870529 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 870639 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_3695188343900049259.key 870639 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_3695188343900049259.key 870639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.9ns 870654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 874642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3695188343900049259.key 874642 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 874758 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8215416168329276086.key 874758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8215416168329276086.key 874758 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.1ns 874758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 878133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8215416168329276086.key 878133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns