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.439s | 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.378s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.377s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.377s | 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.534s | 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.517s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.470s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.486s | 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.486s | 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.299s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.233s | 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.345s | 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.283s | 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.267s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.346s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.407s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.332s | 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.877s | 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.359s | 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.392s | 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.346s | 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.347s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.408s | 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.393s | 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.376s | passed |
Standard output
725304 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 725304 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 725304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 725320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 728807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 728822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 729432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.63ms 729541 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11766674538542686901.key 729541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11766674538542686901.key 729541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 456ns 729541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 733278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 733309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11766674538542686901.key 733309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 733419 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 733419 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 733419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.2ns 733419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 736592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 736607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 736670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.07ms 736779 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3690076273415129747.key 736779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3690076273415129747.key 736779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.3ns 736779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 740047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 740063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3690076273415129747.key 740063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 740172 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_40775399487227879.key 740172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_40775399487227879.key 740172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.8ns 740172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 743378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 743409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_40775399487227879.key 743409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 743518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7512015244870014866.key 743518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7512015244870014866.key 743518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.1ms 743518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 746723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 746739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7512015244870014866.key 746755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.1ns 746865 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_134801715701622111.key 746865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_134801715701622111.key 746865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.3ns 746865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 750164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_134801715701622111.key 750164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 750273 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11260416726088525038.key 750273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11260416726088525038.key 750273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.3ns 750273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 753525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 753541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11260416726088525038.key 753557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.1ns 753666 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_4254310407085141990.key 753666 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_4254310407085141990.key 753666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.9ns 753666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 756934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4254310407085141990.key 756934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 757043 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5434978761643674504.key 757043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5434978761643674504.key 757043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 757043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 760342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 760373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5434978761643674504.key 760373 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 760482 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 760482 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 760482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.7ns 760482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 763719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 763751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 763751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 763860 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12224977850930400446.key 763860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12224977850930400446.key 763860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.8ns 763860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 767128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12224977850930400446.key 767128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 767237 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1830605057586933808.key 767237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1830605057586933808.key 767237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.3ns 767237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 770489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 770504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_1830605057586933808.key 770504 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 770614 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10095511644177477843.key 770614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10095511644177477843.key 770614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 770614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 774023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 774038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10095511644177477843.key 774038 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 774148 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8718012285725355259.key 774148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8718012285725355259.key 774148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 412ns 774163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 777541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 777556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8718012285725355259.key 777556 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 777666 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2043699792388544605.key 777666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2043699792388544605.key 777666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.2ns 777666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 781012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_2043699792388544605.key 781012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 781137 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5696330638884125987.key 781137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5696330638884125987.key 781137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.1ns 781137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 784499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 784514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5696330638884125987.key 784514 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 784624 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2364411920945644443.key 784624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2364411920945644443.key 784624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.1ns 784624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 787986 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 788001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2364411920945644443.key 788001 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 788111 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6856584214666008562.key 788111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6856584214666008562.key 788111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 686.2ns 788111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791270 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 791301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6856584214666008562.key 791301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 791410 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12041044646954040439.key 791410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12041044646954040439.key 791410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 428ns 791410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 794646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12041044646954040439.key 794646 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 794756 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11318567247171258021.key 794756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11318567247171258021.key 794756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.1ns 794756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 797929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11318567247171258021.key 797929 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 798039 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_15833107772056405187.key 798039 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_15833107772056405187.key 798039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 798039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 801197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_15833107772056405187.key 801197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 801307 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11933651862503015392.key 801307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11933651862503015392.key 801307 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 801307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 804543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11933651862503015392.key 804543 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 804653 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_1391983366919901266.key 804653 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_1391983366919901266.key 804653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248ns 804653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 807951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1391983366919901266.key 807951 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 808060 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12312978958655840525.key 808060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12312978958655840525.key 808060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 808060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 811282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12312978958655840525.key 811282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns