ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m25.42s

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.430s 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.481s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.430s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.454s 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.467s 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.590s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.400s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.345s 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.410s 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.321s 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.528s 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.219s 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.275s 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.310s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.284s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.321s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.256s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.562s 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.500s 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.439s 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.515s 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.369s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.462s 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.509s 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.545s passed

Standard output

778592     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_15478883323180417357.key 
778593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_15478883323180417357.key 
778593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
778599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
782016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15478883323180417357.key 
782018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
782120     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 
782121     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 
782121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
782122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
785571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
785579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
785681     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 
785682     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 
785682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
785683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
789052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
789079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.73ms 
789182     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_12903663961107122877.key 
789182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_12903663961107122877.key 
789182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
789183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
792518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12903663961107122877.key 
792519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
792622     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_14052303968949447307.key 
792622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_14052303968949447307.key 
792623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
792625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
796029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14052303968949447307.key 
796031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
796137     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_13670884929135075307.key 
796137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_13670884929135075307.key 
796138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
796138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
799401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13670884929135075307.key 
799403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
799506     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_9120641609405549265.key 
799506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_9120641609405549265.key 
799506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
799507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
802863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9120641609405549265.key 
802864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
802967     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_8783728135854102229.key 
802967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_8783728135854102229.key 
802967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
802968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
806372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_8783728135854102229.key 
806373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
806477     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_8404661247504464764.key 
806477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_8404661247504464764.key 
806477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
806478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
809917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_8404661247504464764.key 
809918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
810021     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_7747438131547589104.key 
810021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_7747438131547589104.key 
810021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
810022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
813347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7747438131547589104.key 
813349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
813451     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 
813451     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 
813452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.1ns 
813453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
816824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
816829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
816932     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_14314716308897156657.key 
816933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_14314716308897156657.key 
816934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.32ms 
816935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
820259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14314716308897156657.key 
820260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
820362     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_2806341725633550762.key 
820363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_2806341725633550762.key 
820363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
820364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
823712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2806341725633550762.key 
823713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
823816     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_15040470699770038755.key 
823816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_15040470699770038755.key 
823817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
823818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
827178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_15040470699770038755.key 
827180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
827283     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_3397209733484984767.key 
827284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_3397209733484984767.key 
827284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
827285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
830768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3397209733484984767.key 
830770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
830873     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_3043792300743997044.key 
830874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_3043792300743997044.key 
830874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
830875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
834162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3043792300743997044.key 
834164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
834273     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_6508845777671107875.key 
834273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_6508845777671107875.key 
834273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
834274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
837497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
837514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6508845777671107875.key 
837515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
837618     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_3605061494563325280.key 
837618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_3605061494563325280.key 
837618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
837619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
840924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3605061494563325280.key 
840925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 
841028     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_11629282272029739052.key 
841028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_11629282272029739052.key 
841028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
841030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
844245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11629282272029739052.key 
844246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
844349     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_11387942405707127476.key 
844349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_11387942405707127476.key 
844349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
844350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
847447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
847463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11387942405707127476.key 
847464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
847568     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_16645568924945898632.key 
847569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_16645568924945898632.key 
847569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
847570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
850737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16645568924945898632.key 
850741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
850844     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_13233086902804320797.key 
850844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_13233086902804320797.key 
850845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 594ns 
850846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
854033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
854049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13233086902804320797.key 
854050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
854153     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_12934717160714000702.key 
854153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_12934717160714000702.key 
854153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
854154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
857318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
857334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12934717160714000702.key 
857335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
857438     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_14338853329258459606.key 
857439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_14338853329258459606.key 
857439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.2ns 
857440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
860638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
860655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14338853329258459606.key 
860656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
860759     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_4892210952374948741.key 
860759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_4892210952374948741.key 
860759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
860760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
863893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
863908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4892210952374948741.key 
863912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns