ProveSMTLemmasTest

all > de.uka.ilkd.key.smt.newsmt2 > ProveSMTLemmasTest
25

tests
0

failures
0

ignored
1m16.09s

duration
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.948s 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.127s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.046s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.983s 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.926s 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.947s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.105s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.029s 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.012s 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.043s 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] 3.055s 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.157s 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.126s 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.138s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.081s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.128s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.117s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 2.990s 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.975s 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.055s 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.051s 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.036s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.986s 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.070s 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.963s passed

Standard output

675332     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_14325776148211580114.key 
675333     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSub.dl_14325776148211580114.key 
676287     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
678283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
678283     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSub.dl_14325776148211580114.key 
678388     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 
678388     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
679345     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
681275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
681275     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
681378     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 
681378     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
682316     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
684251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
684251     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
684353     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_5355274577794206172.key 
684354     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_singleton.dl_5355274577794206172.key 
685299     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
687306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
687306     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_singleton.dl_5355274577794206172.key 
687408     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_16486494611195588174.key 
687408     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_create.dl_16486494611195588174.key 
688352     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
690356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
690356     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_create.dl_16486494611195588174.key 
690459     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_3788958300702705185.key 
690459     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_allFields.dl_3788958300702705185.key 
691431     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
693392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
693393     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_allFields.dl_3788958300702705185.key 
693495     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_4839393622263937564.key 
693495     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqEmpty.dl_4839393622263937564.key 
694422     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
696378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
696379     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqEmpty.dl_4839393622263937564.key 
696481     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_13092439637077901076.key 
696481     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_union.dl_13092439637077901076.key 
697351     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
699448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
699449     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_union.dl_13092439637077901076.key 
699551     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_10401155226630196447.key 
699551     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqConcat.dl.2_10401155226630196447.key 
700460     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
702412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
702412     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqConcat.dl.2_10401155226630196447.key 
702514     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_16181605992230146742.key 
702514     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_wellFormed.dl_16181605992230146742.key 
703382     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
705360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
705360     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_wellFormed.dl_16181605992230146742.key 
705462     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 
705462     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
706383     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
708479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
708480     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
708589     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_2516579730083098640.key 
708589     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_empty.dl_2516579730083098640.key 
709496     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
711532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
711532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_empty.dl_2516579730083098640.key 
711635     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_5308059852346090365.key 
711635     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_allLocs.dl_5308059852346090365.key 
712528     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
714515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
714515     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_allLocs.dl_5308059852346090365.key 
714618     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_5573603970227675459.key 
714618     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_arrayRange.dl_5573603970227675459.key 
715503     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
717441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 
717441     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_arrayRange.dl_5573603970227675459.key 
717544     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_3208621838267442694.key 
717544     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqConcat.dl_3208621838267442694.key 
718408     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
720388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
720389     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqConcat.dl_3208621838267442694.key 
720492     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_17727994609380872042.key 
720492     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqLen.dl_17727994609380872042.key 
721417     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
723494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
723494     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqLen.dl_17727994609380872042.key 
723597     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_3597079980231821470.key 
723597     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_length.dl_3597079980231821470.key 
724521     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
726522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
726523     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_length.dl_3597079980231821470.key 
726625     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_13204647655145009418.key 
726625     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_freshLocs.dl_13204647655145009418.key 
727539     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
729534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
729534     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_freshLocs.dl_13204647655145009418.key 
729636     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_8708176515698850579.key 
729637     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_anon.dl_8708176515698850579.key 
730522     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
732578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 
732578     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_anon.dl_8708176515698850579.key 
732680     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_17172560949386300424.key 
732680     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_memset.dl_17172560949386300424.key 
733625     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
735734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
735734     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_memset.dl_17172560949386300424.key 
735837     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_4853166319865783289.key 
735837     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_store.dl_4853166319865783289.key 
736901     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
738861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
738861     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_store.dl_4853166319865783289.key 
738963     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_1795594858558496183.key 
738963     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSub.dl.2_1795594858558496183.key 
739930     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
741999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
741999     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSub.dl.2_1795594858558496183.key 
742101     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6039179116104427667.key 
742102     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSingleton.dl_6039179116104427667.key 
743049     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
745079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
745080     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSingleton.dl_6039179116104427667.key 
745182     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_5136416601434307362.key 
745183     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSingleton.dl.2_5136416601434307362.key 
746155     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
748207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
748208     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_seqSingleton.dl.2_5136416601434307362.key 
748310     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_11098128393230145755.key 
748310     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_null.dl_11098128393230145755.key 
749259     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
751325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
751325     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file /tmp/SMT_lemma_null.dl_11098128393230145755.key