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.396s | 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.406s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.391s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.250s | 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.252s | 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.308s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.380s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.269s | 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.369s | 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.239s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.321s | 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.235s | 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.244s | 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.362s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.315s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.250s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.366s | 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.276s | 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.469s | 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.307s | 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.290s | 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.401s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.254s | 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.221s | 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.236s | passed |
Standard output
773420 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 773420 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 773420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 773420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 776621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 776637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 776637 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 776746 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13062236876626366742.key 776746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13062236876626366742.key 776746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.5ns 776746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 779888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 779904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13062236876626366742.key 779920 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 780022 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 780022 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 780022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.2ns 780022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 783221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 783252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 783377 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.61ms 783491 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7185753242900108917.key 783491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7185753242900108917.key 783491 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.5ns 783491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 786664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 786680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7185753242900108917.key 786680 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 223.7ns 786798 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8986342446642363790.key 786798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8986342446642363790.key 786798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.4ns 786798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 789978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8986342446642363790.key 789978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 790088 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14381755362228864375.key 790088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14381755362228864375.key 790088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.5ns 790088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 793364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 793380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14381755362228864375.key 793380 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 793489 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14565306079676327172.key 793489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14565306079676327172.key 793489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.4ns 793489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 796619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_14565306079676327172.key 796634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 796743 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14506842204707805493.key 796743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14506842204707805493.key 796743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.2ns 796743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 799848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_14506842204707805493.key 799848 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 799964 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_14193145096165532616.key 799964 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_14193145096165532616.key 799964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.3ns 799964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 803070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 803086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_14193145096165532616.key 803086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 803200 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5241296317777557633.key 803200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5241296317777557633.key 803200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.7ns 803200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806471 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 806487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5241296317777557633.key 806487 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 806596 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 806627 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 806627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.7ns 806643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 809892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 809892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957ns 810002 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14394398394708357381.key 810002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14394398394708357381.key 810002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 810002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 813284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14394398394708357381.key 813284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 813394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8693966423992795191.key 813394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8693966423992795191.key 813394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 982.8ns 813394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 816529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8693966423992795191.key 816529 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 816644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10425817942964149313.key 816644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10425817942964149313.key 816644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.7ns 816644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819770 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 819786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10425817942964149313.key 819786 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 819896 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4391069722681667324.key 819896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4391069722681667324.key 819896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.6ns 819896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 823094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4391069722681667324.key 823094 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ns 823204 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12695007721125202886.key 823204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12695007721125202886.key 823204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.6ns 823204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 826410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 826425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12695007721125202886.key 826456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 826585 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_494136659597913828.key 826585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_494136659597913828.key 826585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 826585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 829728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_494136659597913828.key 829744 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 829854 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_275140622358730288.key 829854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_275140622358730288.key 829854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.4ns 829854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 833113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_275140622358730288.key 833113 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ns 833223 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15879325985874687566.key 833223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15879325985874687566.key 833223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377ns 833223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 836335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 836350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15879325985874687566.key 836350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 836463 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13386555051233827189.key 836463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13386555051233827189.key 836463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.2ns 836463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 839583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13386555051233827189.key 839583 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 839699 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3220308968595427475.key 839699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3220308968595427475.key 839699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.6ns 839699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 842834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3220308968595427475.key 842834 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 842943 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_8316349393931479001.key 842943 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_8316349393931479001.key 842943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 842943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 846180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 846195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8316349393931479001.key 846195 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 846305 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17175509721902655644.key 846305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17175509721902655644.key 846305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.5ns 846305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 849496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17175509721902655644.key 849496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 849621 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_7443910654984327914.key 849621 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_7443910654984327914.key 849621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 849636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 852736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 852751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7443910654984327914.key 852767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 852876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9353347447929067867.key 852876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9353347447929067867.key 852876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.1ns 852876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 856127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9353347447929067867.key 856127 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns