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.033s | 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.079s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.080s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.033s | 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.018s | 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.079s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.095s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.254s | 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.267s | 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.221s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.675s | 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.252s | 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.282s | 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.284s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.330s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.203s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.501s | 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.549s | 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.813s | 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.673s | 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.596s | 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.422s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.206s | 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.281s | 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.252s | passed |
Standard output
822605 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 822621 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 822621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 822621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 826138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 826170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 826170 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.42ms 826279 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6757317300423487836.key 826279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6757317300423487836.key 826279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns 826279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 829703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6757317300423487836.key 829719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 829828 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 829828 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 829828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.6ns 829828 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 833471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 833533 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.77ms 833642 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7267029570404910424.key 833642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7267029570404910424.key 833642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.1ns 833642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 837207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7267029570404910424.key 837207 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 837316 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3532963222200541767.key 837316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3532963222200541767.key 837316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 837316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 840787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3532963222200541767.key 840803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 840912 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11743047677196598680.key 840912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11743047677196598680.key 840912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.7ns 840912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 844227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_11743047677196598680.key 844227 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 844336 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10585035574840822677.key 844336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10585035574840822677.key 844336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.1ns 844336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 847432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10585035574840822677.key 847432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 847542 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7260317242111505410.key 847542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7260317242111505410.key 847542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.7ns 847542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 850699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7260317242111505410.key 850699 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 850824 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_17864736933990355612.key 850824 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_17864736933990355612.key 850824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 649.9ns 850824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 853967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17864736933990355612.key 853967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 854076 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3701790070298060130.key 854076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3701790070298060130.key 854076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 854076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 856999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3701790070298060130.key 856999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 857109 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 857109 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 857109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.4ns 857109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 860079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 860079 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 860188 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9547465327393035480.key 860188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9547465327393035480.key 860188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.5ns 860188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 863159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9547465327393035480.key 863159 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 863268 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6973766489909663537.key 863268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6973766489909663537.key 863268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252ns 863268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 866160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 866191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6973766489909663537.key 866191 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 866301 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4048053211105699027.key 866301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4048053211105699027.key 866301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.8ns 866301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 869209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_4048053211105699027.key 869209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 869319 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8627620978582193162.key 869319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8627620978582193162.key 869319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.9ns 869319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 872289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8627620978582193162.key 872289 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 872398 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3909853871061469250.key 872398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3909853871061469250.key 872398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 872398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 875369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 875384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3909853871061469250.key 875384 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 875494 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5003739313665124470.key 875494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5003739313665124470.key 875494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.7ns 875494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 878641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5003739313665124470.key 878641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 878749 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17860010582657826302.key 878749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17860010582657826302.key 878749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.1ns 878749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 881891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17860010582657826302.key 881891 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 882016 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2087082959169648785.key 882016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2087082959169648785.key 882016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.2ns 882016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 885128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2087082959169648785.key 885128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 885237 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8911470138500021886.key 885237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8911470138500021886.key 885237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.9ns 885237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 888364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8911470138500021886.key 888364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 888489 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16517902594067510945.key 888489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16517902594067510945.key 888489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.9ns 888489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 891647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16517902594067510945.key 891663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 891772 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_16885074260796001340.key 891772 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_16885074260796001340.key 891772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.9ns 891772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 894915 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 894930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16885074260796001340.key 894946 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 895056 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17441321501878236961.key 895056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17441321501878236961.key 895056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.1ns 895056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 898276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17441321501878236961.key 898276 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ns 898386 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_18406340537421159413.key 898386 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_18406340537421159413.key 898386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 898386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 901450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 901465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_18406340537421159413.key 901482 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 901590 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17301316361200684250.key 901590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17301316361200684250.key 901590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316ns 901590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 904968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 904983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17301316361200684250.key 904983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns