ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m8.93s

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.875s 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.689s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.721s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.689s 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.703s 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.688s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.705s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.680s 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.720s 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.704s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 2.900s 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.736s 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.720s 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.752s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.721s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.736s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.705s 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.773s 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.907s 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.751s 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.830s 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.736s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.891s 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.767s 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.829s passed

Standard output

639796     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 
639796     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 
639796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
639796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
642575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
642591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
642701     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7082152092616965532.key 
642701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7082152092616965532.key 
642701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224ns 
642701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
645359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_7082152092616965532.key 
645359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
645468     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 
645468     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 
645468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.8ns 
645468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
648235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
648266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.63ms 
648376     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13945010794712187895.key 
648376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13945010794712187895.key 
648376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.5ns 
648376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
651018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13945010794712187895.key 
651018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
651127     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16227660775232266338.key 
651127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16227660775232266338.key 
651127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.2ns 
651127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
653849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16227660775232266338.key 
653849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
653958     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5353326505925620476.key 
653958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5353326505925620476.key 
653958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.4ns 
653958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
656584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_5353326505925620476.key 
656584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
656694     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8122126962498491432.key 
656694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8122126962498491432.key 
656694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.5ns 
656694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
659476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8122126962498491432.key 
659476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
659585     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14835298797343416077.key 
659585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14835298797343416077.key 
659585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324ns 
659585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
662243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_14835298797343416077.key 
662243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
662353     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_8573877588035692158.key 
662353     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_8573877588035692158.key 
662353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.1ns 
662353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
665073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_8573877588035692158.key 
665073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
665182     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6076083902343327284.key 
665182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6076083902343327284.key 
665198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 20.22ms 
665198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
667949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6076083902343327284.key 
667949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
668058     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 
668058     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 
668058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.2ns 
668058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
670622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
670638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
670747     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3744823695264822251.key 
670747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3744823695264822251.key 
670747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.7ns 
670747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
673358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3744823695264822251.key 
673358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
673468     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3796969244367823712.key 
673468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3796969244367823712.key 
673468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.3ns 
673468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
676047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_3796969244367823712.key 
676047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
676156     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2135680248835736064.key 
676156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2135680248835736064.key 
676156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 
676156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
678735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2135680248835736064.key 
678751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
678860     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7775710108373831845.key 
678860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7775710108373831845.key 
678860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.2ns 
678860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
681439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7775710108373831845.key 
681439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
681549     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14166592571106543937.key 
681549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14166592571106543937.key 
681549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.8ns 
681549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
684144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14166592571106543937.key 
684144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
684254     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2539134667582699703.key 
684254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2539134667582699703.key 
684254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
684254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
686835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2539134667582699703.key 
686835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
686935     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7706720872547527981.key 
686935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7706720872547527981.key 
686935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.9ns 
686935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
689546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7706720872547527981.key 
689546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ns 
689655     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11632730635480349758.key 
689655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11632730635480349758.key 
689655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.4ns 
689655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
692250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11632730635480349758.key 
692250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
692359     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14452508415947928132.key 
692359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14452508415947928132.key 
692359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 
692359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
694987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14452508415947928132.key 
694987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
695096     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1066092062081287481.key 
695096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1066092062081287481.key 
695096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.9ns 
695096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
697707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1066092062081287481.key 
697707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
697817     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_4337324878412756455.key 
697817     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_4337324878412756455.key 
697817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns 
697817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
700443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4337324878412756455.key 
700443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
700568     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7825826878823918082.key 
700568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7825826878823918082.key 
700568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.6ns 
700568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
703179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7825826878823918082.key 
703179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
703289     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_8343026896065869354.key 
703289     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_8343026896065869354.key 
703289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.3ns 
703289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
705916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8343026896065869354.key 
705916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
706025     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_16621168011038673244.key 
706025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_16621168011038673244.key 
706025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
706025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
708621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_16621168011038673244.key 
708621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns