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.470s | 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.534s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.720s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.581s | 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.548s | 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.595s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.486s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.534s | 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.663s | 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.394s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.798s | 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.453s | 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.503s | 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.456s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.361s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.377s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.328s | 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.689s | 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.659s | 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.611s | 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.674s | 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.611s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.549s | 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.549s | 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.581s | passed |
Standard output
845631 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 845631 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 846850 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 849320 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 849430 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10077238442660705052.key 849430 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10077238442660705052.key 850619 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 853010 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10077238442660705052.key 853119 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 853119 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 854260 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 856668 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 856778 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10700258006558367420.key 856778 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10700258006558367420.key 857919 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 860279 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10700258006558367420.key 860389 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2939294401085350369.key 860389 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2939294401085350369.key 861530 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 863953 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2939294401085350369.key 864063 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9101755098507354411.key 864063 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9101755098507354411.key 865204 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 867549 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9101755098507354411.key 867674 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9831762666505986621.key 867674 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9831762666505986621.key 868768 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 871114 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9831762666505986621.key 871223 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3027058792832862835.key 871223 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3027058792832862835.key 872317 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 874663 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3027058792832862835.key 874772 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_6125300823431561794.key 874772 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_6125300823431561794.key 875902 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 878244 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_6125300823431561794.key 878354 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18335385140095971148.key 878354 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18335385140095971148.key 879448 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 881715 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18335385140095971148.key 881824 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 881824 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 882950 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 885248 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 885358 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4492159237558785654.key 885358 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4492159237558785654.key 886483 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 888969 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4492159237558785654.key 889078 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3506838360018413400.key 889078 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3506838360018413400.key 890220 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 892550 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3506838360018413400.key 892659 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14975575172956741303.key 892659 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14975575172956741303.key 893816 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 896098 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14975575172956741303.key 896207 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10551661400175876632.key 896207 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10551661400175876632.key 897318 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 899694 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10551661400175876632.key 899803 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14195370566929525008.key 899803 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14195370566929525008.key 900914 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 903181 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14195370566929525008.key 903290 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15268543334701787849.key 903290 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15268543334701787849.key 904384 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 906715 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15268543334701787849.key 906824 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5210288102217441667.key 906824 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5210288102217441667.key 907950 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 910378 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5210288102217441667.key 910487 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4548458147500153030.key 910487 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4548458147500153030.key 911551 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 913771 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4548458147500153030.key 913881 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11090262650588211448.key 913881 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11090262650588211448.key 914960 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 917226 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11090262650588211448.key 917335 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9551176721269185861.key 917335 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9551176721269185861.key 918383 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 920728 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9551176721269185861.key 920838 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_6433476197051230863.key 920838 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_6433476197051230863.key 921870 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 924184 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_6433476197051230863.key 924294 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3091181991657238443.key 924294 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3091181991657238443.key 925294 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 927545 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3091181991657238443.key 927655 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_10583158354418941181.key 927655 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_10583158354418941181.key 928655 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 930922 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_10583158354418941181.key 931032 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12201221521104990265.key 931032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12201221521104990265.key 932032 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 934252 DEBUG Test worker d.u.i.k.p.i.KeYFile Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12201221521104990265.key