ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m18.51s

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] 3.121s 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.080s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.042s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.070s passed
[14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) testSMTLemmaSoundness(String, String)[14] 3.093s passed
[15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) testSMTLemmaSoundness(String, String)[15] 3.096s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.068s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.094s 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.101s 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.112s 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.164s 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.105s 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.081s 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.098s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.130s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.148s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.131s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.122s passed
[3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) testSMTLemmaSoundness(String, String)[3] 3.421s 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.212s 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.228s 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.243s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.120s 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.176s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 3.256s passed

Standard output

760566     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_4359224349614685924.key 
760566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_4359224349614685924.key 
760567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.8ns 
760568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
763625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4359224349614685924.key 
763626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
763729     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 
763730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
763730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
763731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
766736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
766748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
766851     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 
766852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
766852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
766856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
770138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
770169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.17ms 
770272     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_2551700888072365502.key 
770272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_2551700888072365502.key 
770273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
770278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
773377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_2551700888072365502.key 
773378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
773484     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_3276357921271639186.key 
773484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_3276357921271639186.key 
773484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns 
773485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
776608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3276357921271639186.key 
776610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
776712     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_3650788826917954131.key 
776712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_3650788826917954131.key 
776713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
776714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
779851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3650788826917954131.key 
779853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
779956     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_3074198525313457193.key 
779956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_3074198525313457193.key 
779957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
779959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
782971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3074198525313457193.key 
782973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
783075     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_17706737496227168711.key 
783076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_17706737496227168711.key 
783076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
783077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
786147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17706737496227168711.key 
786149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
786251     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_1716477089338355679.key 
786252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_1716477089338355679.key 
786252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
786253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
789403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1716477089338355679.key 
789405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
789507     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_15310611428115861768.key 
789507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_15310611428115861768.key 
789508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 663.5ns 
789511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
792521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15310611428115861768.key 
792522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
792627     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 
792628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
792628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
792629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
795601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
795606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
795709     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_2635001413625385894.key 
795709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_2635001413625385894.key 
795709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
795710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
798646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2635001413625385894.key 
798648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
798751     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_11487838939624431334.key 
798751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_11487838939624431334.key 
798751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
798752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
801716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11487838939624431334.key 
801718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
801820     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_7727254907435679926.key 
801821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_7727254907435679926.key 
801821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
801822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
804809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_7727254907435679926.key 
804810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.5ns 
804913     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_7219022830673392067.key 
804913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_7219022830673392067.key 
804913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
804915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
807905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7219022830673392067.key 
807906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
808010     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_8274569413515056310.key 
808010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_8274569413515056310.key 
808010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
808011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
810973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8274569413515056310.key 
810974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
811079     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_2905855573869781890.key 
811080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_2905855573869781890.key 
811080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.9ns 
811081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
814069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2905855573869781890.key 
814071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.2ns 
814173     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_3675246600492212453.key 
814174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_3675246600492212453.key 
814174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
814175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
817170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3675246600492212453.key 
817172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ns 
817274     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_5746396547616161944.key 
817275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_5746396547616161944.key 
817275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
817276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
820282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5746396547616161944.key 
820283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
820387     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_7365333308835231022.key 
820387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_7365333308835231022.key 
820387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
820388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
823387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7365333308835231022.key 
823389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
823491     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_12030037734306655807.key 
823492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_12030037734306655807.key 
823492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
823493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
826468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12030037734306655807.key 
826469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
826572     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_13699867793413115931.key 
826573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_13699867793413115931.key 
826573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
826575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
829566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13699867793413115931.key 
829567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
829670     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_5708233959305583564.key 
829670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_5708233959305583564.key 
829670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
829671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
832680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
832696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5708233959305583564.key 
832697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
832800     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_344319701333412475.key 
832800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_344319701333412475.key 
832800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
832801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
835844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_344319701333412475.key 
835846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
835948     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_8427472553169792315.key 
835948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_8427472553169792315.key 
835949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
835949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
838975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8427472553169792315.key 
838976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns