ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m21.16s

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.227s 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.217s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.100s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.201s 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.141s 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.147s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.261s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.308s 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.253s 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.167s 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.450s 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.143s 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.126s 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.206s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.161s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.228s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.161s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.351s 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.432s 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.403s 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.408s 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.348s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.250s 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.244s 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.228s passed

Standard output

761527     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_6965036229882223881.key 
761528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_6965036229882223881.key 
761528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
761530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
764873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6965036229882223881.key 
764874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
764977     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 
764977     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 
764977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
764978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
768218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
768225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
768328     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 
768332     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 
768332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.41ns 
768335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
771629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
771653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 
771761     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_9472245917434057229.key 
771761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_9472245917434057229.key 
771761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
771762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
775057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9472245917434057229.key 
775060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
775163     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_2056465546173922456.key 
775163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_2056465546173922456.key 
775163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
775164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
778467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2056465546173922456.key 
778468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
778571     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_15938959189287104755.key 
778571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_15938959189287104755.key 
778571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
778572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
781816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15938959189287104755.key 
781817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ns 
781919     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_15601517873071424845.key 
781920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_15601517873071424845.key 
781920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
781921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
785065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15601517873071424845.key 
785066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
785169     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_1878027315459597825.key 
785169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_1878027315459597825.key 
785169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
785170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
788310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1878027315459597825.key 
788311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
788413     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_7147060501300368601.key 
788414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_7147060501300368601.key 
788414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
788415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
791537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7147060501300368601.key 
791539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
791641     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_851072433952915126.key 
791641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_851072433952915126.key 
791641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
791642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
794765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_851072433952915126.key 
794766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
794868     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 
794868     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 
794868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
794870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
797977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
797981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
798085     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_3841355786628044629.key 
798085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_3841355786628044629.key 
798085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
798086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
801081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3841355786628044629.key 
801083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
801185     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_16272011332539987236.key 
801185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_16272011332539987236.key 
801185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
801186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
804283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_16272011332539987236.key 
804284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
804387     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_18296286439705917587.key 
804387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_18296286439705917587.key 
804387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
804388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
807423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_18296286439705917587.key 
807424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
807526     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_15372236021435846524.key 
807527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_15372236021435846524.key 
807527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
807529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
810571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15372236021435846524.key 
810572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
810675     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_7199209148376319435.key 
810675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_7199209148376319435.key 
810675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
810676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
813831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7199209148376319435.key 
813832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
813935     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_14147401030466565427.key 
813935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_14147401030466565427.key 
813935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
813936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
817140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_14147401030466565427.key 
817141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
817243     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_8270027582354834397.key 
817243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_8270027582354834397.key 
817243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
817244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
820392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8270027582354834397.key 
820393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 
820496     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_4181955364144986956.key 
820496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_4181955364144986956.key 
820496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
820497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
823558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4181955364144986956.key 
823560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
823663     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_291876749540608779.key 
823663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_291876749540608779.key 
823663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
823665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
826702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_291876749540608779.key 
826703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
826806     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_11644634299808939931.key 
826807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_11644634299808939931.key 
826807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
826808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
829827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11644634299808939931.key 
829829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
829932     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_2223664610432662919.key 
829932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_2223664610432662919.key 
829932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
829933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
833031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2223664610432662919.key 
833032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
833138     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6158247940344745266.key 
833139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_6158247940344745266.key 
833139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
833139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
836195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6158247940344745266.key 
836196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
836299     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_7960820497138813158.key 
836299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_7960820497138813158.key 
836299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
836300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
839423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7960820497138813158.key 
839424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
839527     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_5684751550930260634.key 
839527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_5684751550930260634.key 
839527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
839528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
842570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
842584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5684751550930260634.key 
842586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns