ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m6.77s

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.673s 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.690s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.657s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.688s 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.643s 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.689s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.704s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.658s 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.673s 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.673s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 2.692s 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.642s 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.673s 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.673s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.689s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.641s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.688s 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] 2.642s 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.657s 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.673s 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.673s 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.660s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.672s 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.690s 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.657s passed

Standard output

627922     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 
627922     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 
627922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
627938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
630501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
630517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
630627     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6668395445950214232.key 
630627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6668395445950214232.key 
630627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.4ns 
630627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
633160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6668395445950214232.key 
633160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
633269     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 
633269     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 
633269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.1ns 
633269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
635802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
635818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
635927     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15088741576935260953.key 
635927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15088741576935260953.key 
635927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.4ns 
635927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
638491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15088741576935260953.key 
638491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 
638600     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7927144704814282548.key 
638600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7927144704814282548.key 
638600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.9ns 
638600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
641165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7927144704814282548.key 
641165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 
641274     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8787528912139632390.key 
641274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8787528912139632390.key 
641274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.8ns 
641274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
643808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8787528912139632390.key 
643808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
643933     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10771997025241065609.key 
643933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10771997025241065609.key 
643933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
643933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
646481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10771997025241065609.key 
646496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
646606     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4411144762465899738.key 
646606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4411144762465899738.key 
646606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
646606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
649186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4411144762465899738.key 
649186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
649296     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_10293222890127275562.key 
649296     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_10293222890127275562.key 
649296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
649296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
651844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10293222890127275562.key 
651844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
651953     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11104546930025593353.key 
651953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11104546930025593353.key 
651953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.1ns 
651953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
654517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11104546930025593353.key 
654517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
654626     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 
654626     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 
654626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.2ns 
654626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
657207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
657207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
657316     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16810066099654209188.key 
657316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16810066099654209188.key 
657316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 
657316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
659865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_16810066099654209188.key 
659865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
659974     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10860963474279842787.key 
659974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10860963474279842787.key 
659974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.2ns 
659974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
662553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10860963474279842787.key 
662553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
662663     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1064171377266113777.key 
662663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1064171377266113777.key 
662663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.8ns 
662663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
665195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_1064171377266113777.key 
665195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
665305     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_643436697035459330.key 
665305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_643436697035459330.key 
665305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.2ns 
665305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
667885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_643436697035459330.key 
667885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
667994     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13121482195248477781.key 
667994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13121482195248477781.key 
667994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
667994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
670589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13121482195248477781.key 
670589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
670699     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11350271827182532952.key 
670699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11350271827182532952.key 
670699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.8ns 
670699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
673248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11350271827182532952.key 
673248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
673358     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4773228334386165162.key 
673358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4773228334386165162.key 
673358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.6ns 
673358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
675922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4773228334386165162.key 
675922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
676031     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17398392643658073676.key 
676031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17398392643658073676.key 
676031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
676031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
678595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17398392643658073676.key 
678595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
678705     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7118423134451202004.key 
678705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7118423134451202004.key 
678705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 
678705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
681238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7118423134451202004.key 
681238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
681347     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3553441911248528085.key 
681347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3553441911248528085.key 
681347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
681347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
683911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3553441911248528085.key 
683911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
684021     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_2886361407768808215.key 
684021     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_2886361407768808215.key 
684021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
684021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
686584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2886361407768808215.key 
686584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
686694     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7217362567361402735.key 
686694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7217362567361402735.key 
686694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.9ns 
686694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
689274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7217362567361402735.key 
689274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
689383     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_17612330859720774989.key 
689383     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_17612330859720774989.key 
689383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.3ns 
689383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
691916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17612330859720774989.key 
691916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
692025     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8672747545506209677.key 
692025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8672747545506209677.key 
692025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.9ns 
692025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
694604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8672747545506209677.key 
694604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns