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] | 5.042s | 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] | 5.052s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.987s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.962s | 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] | 4.985s | 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] | 5.007s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.994s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.001s | 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] | 4.959s | 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] | 5.049s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.074s | 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] | 5.032s | 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] | 5.028s | 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] | 5.018s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.048s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.109s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.080s | 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] | 5.030s | 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] | 5.060s | 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] | 4.989s | 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] | 4.932s | 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] | 5.023s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.007s | 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] | 5.034s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.969s | passed |
Standard output
1155617 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 1155617 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 1155617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 1155617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1160544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1160575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1160575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 1160685 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9197775324810134150.key 1160685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9197775324810134150.key 1160685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393ns 1160685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1165572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1165587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9197775324810134150.key 1165587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1165715 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 1165715 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 1165715 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 1165715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1170617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1170633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1170664 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.6ms 1170775 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4802157365633452900.key 1170775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4802157365633452900.key 1170775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns 1170775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1175639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1175654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4802157365633452900.key 1175654 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1175764 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12709631828153209201.key 1175764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12709631828153209201.key 1175764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.5ns 1175764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1180564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 1180580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12709631828153209201.key 1180580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1180697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8789678768366568987.key 1180697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8789678768366568987.key 1180697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.9ns 1180697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1185595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1185611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8789678768366568987.key 1185611 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1185720 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3568806288211399806.key 1185720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3568806288211399806.key 1185720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.6ns 1185720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1190598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1190613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3568806288211399806.key 1190613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.3ns 1190727 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4476818606640107168.key 1190727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4476818606640107168.key 1190727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.4ns 1190727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1195621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1195636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4476818606640107168.key 1195652 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1195761 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_11248445776879327047.key 1195761 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_11248445776879327047.key 1195761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.2ns 1195761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1200605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 1200621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11248445776879327047.key 1200621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1200730 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12197511000344571600.key 1200730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12197511000344571600.key 1200730 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.6ns 1200730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1205645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1205661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_12197511000344571600.key 1205661 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1205773 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 1205773 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 1205773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.6ns 1205773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1210685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1210700 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1210716 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 1210825 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12012163826258025530.key 1210825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12012163826258025530.key 1210825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.8ns 1210825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1215671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1215702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12012163826258025530.key 1215702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1215812 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_12325181620051628552.key 1215812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_12325181620051628552.key 1215812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.2ns 1215812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1220648 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 1220664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_12325181620051628552.key 1220664 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1220774 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12913870834247279074.key 1220774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12913870834247279074.key 1220774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 1220774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1225629 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1225645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12913870834247279074.key 1225645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1225759 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15070817604077191128.key 1225759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15070817604077191128.key 1225759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.2ns 1225759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1230641 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1230657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15070817604077191128.key 1230657 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1230766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5631630182320893777.key 1230766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5631630182320893777.key 1230766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.5ns 1230766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1235620 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1235636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5631630182320893777.key 1235651 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1235761 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11281082937595340327.key 1235761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11281082937595340327.key 1235761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 1235761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1240616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1240632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11281082937595340327.key 1240647 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1240762 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4375618412497309649.key 1240762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4375618412497309649.key 1240762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.3ns 1240762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1245594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 1245610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4375618412497309649.key 1245610 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.2ns 1245721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15210247495951383624.key 1245721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15210247495951383624.key 1245721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.8ns 1245721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1250642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 1250658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15210247495951383624.key 1250658 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1250770 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14138059289968848451.key 1250770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14138059289968848451.key 1250770 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.3ns 1250770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1255674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1255690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14138059289968848451.key 1255690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1255802 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11275309328020758746.key 1255802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11275309328020758746.key 1255802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.7ns 1255802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1260688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1260703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11275309328020758746.key 1260719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1260830 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_10489974918038116034.key 1260830 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_10489974918038116034.key 1260830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.6ns 1260830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1265723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1265739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10489974918038116034.key 1265739 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1265848 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4377290201619530878.key 1265848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4377290201619530878.key 1265848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.5ns 1265848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1270756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1270772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_4377290201619530878.key 1270788 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1270897 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_5056828484194734674.key 1270897 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_5056828484194734674.key 1270897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 1270897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1275877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1275893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5056828484194734674.key 1275893 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 1276007 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18257116467082100437.key 1276007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18257116467082100437.key 1276007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.7ns 1276007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1280947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1280978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18257116467082100437.key 1280978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns