ProveSMTLemmasTest
|
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.614s | 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.518s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.534s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.549s | 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.612s | 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.503s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.502s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.455s | 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.408s | 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.408s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.660s | 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.424s | 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.424s | 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.394s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.407s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.377s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.360s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 3.550s | 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.752s | 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.565s | 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.438s | 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.440s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.551s | 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.533s | 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.595s | passed |
Standard output
875308 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 875308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 875308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.8ns 875308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 878857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 878857 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 878966 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2304814289190287859.key 878966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2304814289190287859.key 878966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.4ns 878966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 882390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 882406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2304814289190287859.key 882406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 882516 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 882516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 882516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.2ns 882516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 886111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 886127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 886158 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.21ms 886268 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12702033978610668598.key 886268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12702033978610668598.key 886268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.2ns 886268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 889692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 889723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12702033978610668598.key 889723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 889833 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15670491502395344858.key 889833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15670491502395344858.key 889833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.2ns 889833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 893132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 893163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_15670491502395344858.key 893163 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 893272 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14572691809757079435.key 893272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14572691809757079435.key 893272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 893272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 896572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 896588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14572691809757079435.key 896588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 896713 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3037597809556146631.key 896713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3037597809556146631.key 896713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.8ns 896713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 900123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 900154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3037597809556146631.key 900154 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ns 900264 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9498210081708705355.key 900264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9498210081708705355.key 900264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.4ns 900264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 903687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9498210081708705355.key 903687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 903797 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_11035901881118504203.key 903797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_11035901881118504203.key 903797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 568ns 903797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 907268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 907284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11035901881118504203.key 907284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 907393 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3763180985878790918.key 907393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3763180985878790918.key 907393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.7ns 907393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 910882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 910898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3763180985878790918.key 910898 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 911007 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 911007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 911007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.9ns 911007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 914400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 914416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 914416 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 914525 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18219030975139015812.key 914525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18219030975139015812.key 914525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 914525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 917918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 917934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_18219030975139015812.key 917949 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 918059 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15864181664050127630.key 918059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15864181664050127630.key 918059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.2ns 918059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 921467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 921483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15864181664050127630.key 921499 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 921608 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12332533587310036663.key 921608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12332533587310036663.key 921608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285ns 921608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 925095 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 925111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12332533587310036663.key 925111 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 925220 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17139626739693698613.key 925220 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17139626739693698613.key 925220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.2ns 925220 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 928598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 928613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17139626739693698613.key 928613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 928723 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10465240905101060855.key 928723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10465240905101060855.key 928723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.8ns 928723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 932100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 932116 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10465240905101060855.key 932116 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 932226 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9475270274568690509.key 932226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9475270274568690509.key 932226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.4ns 932226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 935555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 935571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9475270274568690509.key 935571 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 935681 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3368076797265665849.key 935681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3368076797265665849.key 935681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.9ns 935681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 938948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 938979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3368076797265665849.key 938979 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ns 939089 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3559338755482938282.key 939089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3559338755482938282.key 939089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.7ns 939089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 942357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 942388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3559338755482938282.key 942388 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 942497 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_315348714037810304.key 942497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_315348714037810304.key 942497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 942497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 945780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 945796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_315348714037810304.key 945796 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 945921 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3052236934274561887.key 945921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3052236934274561887.key 945921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns 945921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 949220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 949236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3052236934274561887.key 949236 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 949345 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_1131977129646668730.key 949345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_1131977129646668730.key 949345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.1ns 949345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 952599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 952630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1131977129646668730.key 952630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 952740 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11658287112940705298.key 952740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11658287112940705298.key 952740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.2ns 952740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 956023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 956039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11658287112940705298.key 956039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 956148 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_8879531674147002659.key 956148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_8879531674147002659.key 956148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.8ns 956148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 959400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 959415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8879531674147002659.key 959415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 959525 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_16234026577061648904.key 959525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_16234026577061648904.key 959525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.7ns 959525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 962746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 962761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_16234026577061648904.key 962776 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns