ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m3.33s

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.521s 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.528s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.516s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.504s 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.535s 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.518s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.518s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.503s 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.510s 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.524s 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] 2.609s 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.504s 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.503s 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.503s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.530s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.505s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.497s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 2.602s 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.638s 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.571s 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.550s 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.556s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.534s 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.549s 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.505s passed

Standard output

577722     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_8557156321120068941.key 
577722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_8557156321120068941.key 
577723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41ns 
577723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
580225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8557156321120068941.key 
580226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
580331     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 
580332     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 
580332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
580333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
582828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
582831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
582934     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 
582934     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 
582934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
582935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
585460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
585469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
585573     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_5561980736136757868.key 
585574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_5561980736136757868.key 
585574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.5ns 
585575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
588036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5561980736136757868.key 
588037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
588144     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_7540886608215943837.key 
588144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_7540886608215943837.key 
588144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
588145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
590591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7540886608215943837.key 
590592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ns 
590698     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_12448064333567506975.key 
590699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_12448064333567506975.key 
590700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms 
590701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
593150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12448064333567506975.key 
593151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
593254     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_5726233569585447983.key 
593254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_5726233569585447983.key 
593254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
593255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
595685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5726233569585447983.key 
595686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
595788     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_3885800961876414341.key 
595789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_3885800961876414341.key 
595789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
595789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
598233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3885800961876414341.key 
598234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
598337     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_12216775391219663226.key 
598337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_12216775391219663226.key 
598337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
598338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
600739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12216775391219663226.key 
600740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
600843     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_5467864974672571283.key 
600843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_5467864974672571283.key 
600843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
600844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
603259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5467864974672571283.key 
603260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
603363     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 
603364     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 
603364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
603365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
605782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
605784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 961.11ns 
605892     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_12470227802612807494.key 
605892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_12470227802612807494.key 
605893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
605893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
608306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12470227802612807494.key 
608307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
608409     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_6581091433440663718.key 
608409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_6581091433440663718.key 
608409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
608410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
610810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6581091433440663718.key 
610811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
610914     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_2731906402848740060.key 
610914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_2731906402848740060.key 
610914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
610915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
613345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2731906402848740060.key 
613346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
613449     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_17141737822214384647.key 
613449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_17141737822214384647.key 
613449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
613450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
615864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17141737822214384647.key 
615865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
615968     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_6519657083127674055.key 
615968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_6519657083127674055.key 
615969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
615969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
618377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6519657083127674055.key 
618384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
618486     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_13659896280104839269.key 
618487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_13659896280104839269.key 
618487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
618487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
620885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13659896280104839269.key 
620887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
620990     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_6311777866791991198.key 
620991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_6311777866791991198.key 
620991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
620992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
623389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6311777866791991198.key 
623390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ns 
623500     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_12333342783735027788.key 
623500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_12333342783735027788.key 
623500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
623501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
625921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_12333342783735027788.key 
625922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
626024     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_16165001139212358045.key 
626025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_16165001139212358045.key 
626025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
626026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
628426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16165001139212358045.key 
628427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
628530     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_10475253187485699368.key 
628530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_10475253187485699368.key 
628530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
628531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
630930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_10475253187485699368.key 
630931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
631034     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_6073945729645006751.key 
631034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_6073945729645006751.key 
631034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
631035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
633433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6073945729645006751.key 
633434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
633536     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_1440188111831918908.key 
633536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_1440188111831918908.key 
633536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
633537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
635963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1440188111831918908.key 
635964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
636067     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_179106746566631668.key 
636067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_179106746566631668.key 
636067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
636068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
638469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_179106746566631668.key 
638470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
638572     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_12741570785248408408.key 
638573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_12741570785248408408.key 
638573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
638574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
640966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12741570785248408408.key 
640967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns