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] | 2.745s | 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] | 2.753s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.760s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.817s | 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] | 2.745s | 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] | 2.703s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.795s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.821s | 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] | 2.813s | 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] | 2.688s | passed |
| [1] 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)[1] | 2.916s | 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] | 2.779s | 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] | 2.793s | 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] | 2.779s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.814s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.787s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.742s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 2.873s | 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] | 2.896s | 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] | 2.852s | 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] | 2.880s | 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] | 2.874s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.992s | 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] | 2.974s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.823s | passed |
Standard output
646046 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_15103487970586081292.key 646048 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSub.dl_15103487970586081292.key took 0 ms to parse. 646048 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1801 ms. 646941 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 646941 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1802 ms. 648858 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSub.dl_15103487970586081292.key took 0 ms to parse. 648858 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1802 ms. 648960 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 648961 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof took 1 ms to parse. 648961 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1803 ms. 649852 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 649852 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1804 ms. 651730 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof took 0 ms to parse. 651730 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1804 ms. 651834 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 651835 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof took 0 ms to parse. 651836 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1804 ms. 652706 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 652706 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1805 ms. 654624 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof took 0 ms to parse. 654625 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1805 ms. 654731 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_11017243757234831171.key 654731 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_singleton.dl_11017243757234831171.key took 0 ms to parse. 654731 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1805 ms. 655580 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 655580 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1806 ms. 657479 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_singleton.dl_11017243757234831171.key took 0 ms to parse. 657479 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1806 ms. 657583 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_604592510682753187.key 657583 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_create.dl_604592510682753187.key took 0 ms to parse. 657583 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1806 ms. 658443 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 658443 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1807 ms. 660360 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_create.dl_604592510682753187.key took 0 ms to parse. 660361 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1807 ms. 660463 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_11472445820877983445.key 660463 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_allFields.dl_11472445820877983445.key took 0 ms to parse. 660463 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1807 ms. 661334 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 661334 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1808 ms. 663235 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_allFields.dl_11472445820877983445.key took 0 ms to parse. 663235 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1808 ms. 663338 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_11815355422501403152.key 663342 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqEmpty.dl_11815355422501403152.key took 0 ms to parse. 663342 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1808 ms. 664236 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 664237 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1809 ms. 666228 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqEmpty.dl_11815355422501403152.key took 0 ms to parse. 666228 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1809 ms. 666330 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_3043047648543617221.key 666331 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_union.dl_3043047648543617221.key took 0 ms to parse. 666331 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1809 ms. 667356 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 667356 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1810 ms. 669203 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_union.dl_3043047648543617221.key took 0 ms to parse. 669204 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1810 ms. 669305 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_18250584130185069093.key 669306 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqConcat.dl.2_18250584130185069093.key took 0 ms to parse. 669306 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1810 ms. 670166 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 670166 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1811 ms. 672026 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqConcat.dl.2_18250584130185069093.key took 0 ms to parse. 672026 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1811 ms. 672128 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_16937086117200947805.key 672129 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_wellFormed.dl_16937086117200947805.key took 0 ms to parse. 672129 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1811 ms. 672945 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 672945 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1812 ms. 674771 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_wellFormed.dl_16937086117200947805.key took 0 ms to parse. 674771 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1812 ms. 674872 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 674873 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof took 0 ms to parse. 674873 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1812 ms. 675693 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 675693 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1813 ms. 677524 WARN Test worker d.u.i.k.n.ParsingFacade /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof took 0 ms to parse. 677524 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1813 ms. 677626 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_11471693034659516597.key 677626 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_empty.dl_11471693034659516597.key took 0 ms to parse. 677626 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1813 ms. 678432 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 678432 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1814 ms. 680284 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_empty.dl_11471693034659516597.key took 0 ms to parse. 680284 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1814 ms. 680386 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_9711578985980406773.key 680386 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_allLocs.dl_9711578985980406773.key took 0 ms to parse. 680386 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1814 ms. 681277 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 681277 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1815 ms. 683101 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_allLocs.dl_9711578985980406773.key took 0 ms to parse. 683101 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1815 ms. 683203 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_4461304298445670068.key 683204 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_arrayRange.dl_4461304298445670068.key took 1 ms to parse. 683204 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1816 ms. 684059 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 684059 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1817 ms. 685846 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_arrayRange.dl_4461304298445670068.key took 0 ms to parse. 685846 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1817 ms. 685948 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_4745248696566955111.key 685949 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqConcat.dl_4745248696566955111.key took 0 ms to parse. 685949 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1817 ms. 686769 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 3 ms to parse. 686769 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1820 ms. 688549 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqConcat.dl_4745248696566955111.key took 0 ms to parse. 688549 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1820 ms. 688652 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_8346739851914126823.key 688654 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqLen.dl_8346739851914126823.key took 1 ms to parse. 688654 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1821 ms. 689512 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 689514 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1822 ms. 691343 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqLen.dl_8346739851914126823.key took 0 ms to parse. 691343 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1822 ms. 691446 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_1847763247128462352.key 691446 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_length.dl_1847763247128462352.key took 0 ms to parse. 691446 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1822 ms. 692318 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 692318 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1823 ms. 694164 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_length.dl_1847763247128462352.key took 0 ms to parse. 694164 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1823 ms. 694267 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_5324372325555061651.key 694267 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_freshLocs.dl_5324372325555061651.key took 0 ms to parse. 694267 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1823 ms. 695101 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 695102 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1824 ms. 696977 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_freshLocs.dl_5324372325555061651.key took 0 ms to parse. 696977 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1824 ms. 697080 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_17813741245235662462.key 697080 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_anon.dl_17813741245235662462.key took 0 ms to parse. 697080 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1824 ms. 697890 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 697890 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1825 ms. 699666 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_anon.dl_17813741245235662462.key took 0 ms to parse. 699666 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1825 ms. 699768 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_1380236701669485270.key 699769 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_memset.dl_1380236701669485270.key took 0 ms to parse. 699769 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1825 ms. 700598 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 700598 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1826 ms. 702445 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_memset.dl_1380236701669485270.key took 0 ms to parse. 702445 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1826 ms. 702548 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_3873351725492800433.key 702549 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_store.dl_3873351725492800433.key took 1 ms to parse. 702549 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1827 ms. 703413 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 703413 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1828 ms. 705239 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_store.dl_3873351725492800433.key took 0 ms to parse. 705239 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1828 ms. 705342 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_16433710921593119580.key 705343 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSub.dl.2_16433710921593119580.key took 1 ms to parse. 705343 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1829 ms. 706211 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 706211 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1830 ms. 708018 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSub.dl.2_16433710921593119580.key took 0 ms to parse. 708018 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1830 ms. 708120 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6354736508496192736.key 708120 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSingleton.dl_6354736508496192736.key took 0 ms to parse. 708120 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1830 ms. 708945 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 708945 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1831 ms. 710831 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSingleton.dl_6354736508496192736.key took 0 ms to parse. 710831 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1831 ms. 710934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_7921146716097859711.key 710935 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSingleton.dl.2_7921146716097859711.key took 0 ms to parse. 710935 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1831 ms. 711743 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 711743 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1832 ms. 713619 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_seqSingleton.dl.2_7921146716097859711.key took 0 ms to parse. 713620 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1832 ms. 713722 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_2016382091766397971.key 713722 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_null.dl_2016382091766397971.key took 0 ms to parse. 713722 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1832 ms. 714534 WARN Test worker d.u.i.k.n.ParsingFacade file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 1 ms to parse. 714534 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1833 ms. 716362 WARN Test worker d.u.i.k.n.ParsingFacade /tmp/SMT_lemma_null.dl_2016382091766397971.key took 0 ms to parse. 716362 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1833 ms.