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.629s | 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.671s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.705s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.659s | 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.690s | 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.625s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.690s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.751s | 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.721s | 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.705s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.862s | 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.657s | 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.706s | 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.753s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.706s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.627s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.657s | 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.769s | 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.799s | 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.798s | 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.690s | 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.752s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.643s | 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.675s | 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.735s | passed |
Standard output
817205 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 817205 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 817205 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.4ns 817205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 820926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 820941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 821066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4008526521569269517.key 821066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4008526521569269517.key 821066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.1ns 821066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 824726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4008526521569269517.key 824726 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 824836 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 824836 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 824836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.5ns 824836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 828463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 828526 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.63ms 828636 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5524121703927810708.key 828636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5524121703927810708.key 828636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.6ns 828636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 832324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5524121703927810708.key 832324 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.6ns 832434 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9169003481460897983.key 832434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9169003481460897983.key 832434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.6ns 832434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 836014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9169003481460897983.key 836014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 836124 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13372391291013547476.key 836124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13372391291013547476.key 836124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.1ns 836124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 839767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13372391291013547476.key 839767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 839876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12824282344677919512.key 839876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12824282344677919512.key 839876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.9ns 839876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 843394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 843409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12824282344677919512.key 843409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 843519 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16468551415619606761.key 843519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16468551415619606761.key 843519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.6ns 843519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 847084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16468551415619606761.key 847084 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 847194 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_9598498914176420454.key 847194 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_9598498914176420454.key 847194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.4ns 847194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 850821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9598498914176420454.key 850821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 850930 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8584950304624274460.key 850930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8584950304624274460.key 850930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.6ns 850930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 854449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_8584950304624274460.key 854449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 854559 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 854559 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 854559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.3ns 854559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 858122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 858122 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.37ms 858231 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3956165545573434938.key 858231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3956165545573434938.key 858231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.5ns 858231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 861811 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 861827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3956165545573434938.key 861827 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 861936 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_12047312600418027414.key 861936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_12047312600418027414.key 861936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.4ns 861936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865470 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 865486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_12047312600418027414.key 865486 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 865596 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8231524774958145642.key 865596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8231524774958145642.key 865596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.3ns 865596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869161 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 869176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_8231524774958145642.key 869176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 869286 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16706366463391748771.key 869286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16706366463391748771.key 869286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 869286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 872804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_16706366463391748771.key 872804 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 872913 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4566169009857282670.key 872913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4566169009857282670.key 872913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.3ns 872929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 876463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 876479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4566169009857282670.key 876479 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 876604 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17433462865557559506.key 876604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17433462865557559506.key 876604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.6ns 876604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 880231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17433462865557559506.key 880231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 880356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16196284435529376353.key 880371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16196284435529376353.key 880371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.5ns 880371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 883953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 883968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_16196284435529376353.key 883968 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 884078 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1656715024624452392.key 884078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1656715024624452392.key 884078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.8ns 884078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 887658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_1656715024624452392.key 887658 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 887783 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14565988309501170906.key 887783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14565988309501170906.key 887783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.9ns 887783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 891332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14565988309501170906.key 891332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 891441 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4492344072934571744.key 891441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4492344072934571744.key 891441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.3ns 891441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 895037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4492344072934571744.key 895037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 895147 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_16850094531503551383.key 895147 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_16850094531503551383.key 895147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.1ns 895147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 898790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16850094531503551383.key 898790 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 898900 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1446960825205917797.key 898900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1446960825205917797.key 898900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.4ns 898900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 902496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1446960825205917797.key 902496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 902606 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_13934050671031117912.key 902606 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_13934050671031117912.key 902606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 902606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 906124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13934050671031117912.key 906124 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 906233 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4848749442733534509.key 906233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4848749442733534509.key 906233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.3ns 906233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 909782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4848749442733534509.key 909782 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns