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.595s | 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.629s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.502s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.596s | 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.564s | 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.596s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.704s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.556s | 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.549s | 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.549s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.670s | 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.596s | 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.533s | 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.456s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.532s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.522s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.502s | 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.579s | 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.691s | 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.737s | 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.642s | 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.673s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.564s | 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.502s | 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.520s | passed |
Standard output
861374 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 861374 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 861390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.8ns 861390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 864923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 864938 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.19ms 865048 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8539805541814912267.key 865048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8539805541814912267.key 865048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.9ns 865048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 868502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 868518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8539805541814912267.key 868518 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 868627 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 868627 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 868627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.4ns 868627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 872178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 872209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.24ms 872318 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5524601750852871403.key 872318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5524601750852871403.key 872318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 872318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 875929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 875945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5524601750852871403.key 875945 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 876055 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4183152828381113647.key 876055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4183152828381113647.key 876055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.7ns 876055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 879556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 879588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_4183152828381113647.key 879588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 879697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_370062617021369167.key 879697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_370062617021369167.key 879697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.5ns 879697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 883245 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 883261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_370062617021369167.key 883261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 883370 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17661153711335326926.key 883370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17661153711335326926.key 883370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 883370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 886809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 886825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17661153711335326926.key 886825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 886934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10480021760617765578.key 886934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10480021760617765578.key 886934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246ns 886934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 890296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 890327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10480021760617765578.key 890327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 890436 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_5170703135401308242.key 890436 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_5170703135401308242.key 890436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.8ns 890436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 893831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 893847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_5170703135401308242.key 893847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 893956 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7972064367511545753.key 893956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7972064367511545753.key 893956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.7ns 893956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 897411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 897442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7972064367511545753.key 897442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 897551 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 897551 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 897551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 897551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 901040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 901055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 901055 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 901180 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15936271924412041608.key 901180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15936271924412041608.key 901180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.2ns 901180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 904541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 904573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15936271924412041608.key 904573 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 904682 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11562595890115740510.key 904682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11562595890115740510.key 904682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.6ns 904682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 908153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 908168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11562595890115740510.key 908168 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 908278 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13054591258506420809.key 908278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13054591258506420809.key 908278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.9ns 908278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 911701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 911732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13054591258506420809.key 911732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 911842 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13903662996309437414.key 911842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13903662996309437414.key 911842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.2ns 911842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 915328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13903662996309437414.key 915328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 915438 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5970616566005638991.key 915438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5970616566005638991.key 915438 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.6ns 915438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 919033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5970616566005638991.key 919033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 919143 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15600471726396903268.key 919143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15600471726396903268.key 919143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.6ns 919143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 922582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 922598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15600471726396903268.key 922598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 922699 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7676559800677813234.key 922699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_7676559800677813234.key 922699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns 922699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 926107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 926124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7676559800677813234.key 926124 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 926248 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_393717178314173744.key 926248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_393717178314173744.key 926248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.6ns 926248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 929672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 929687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_393717178314173744.key 929687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 929797 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16879345690313764907.key 929797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16879345690313764907.key 929797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.1ns 929797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 933269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 933285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16879345690313764907.key 933285 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 933394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_868036389492350270.key 933394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_868036389492350270.key 933394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213ns 933394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 936802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 936818 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_868036389492350270.key 936818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 936927 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_16713031150008430364.key 936927 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_16713031150008430364.key 936927 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.2ns 936927 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 940242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 940273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16713031150008430364.key 940273 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 940383 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7206492288079206249.key 940383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7206492288079206249.key 940383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.6ns 940383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 943790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 943806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7206492288079206249.key 943806 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 943915 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_3397003476985151750.key 943915 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_3397003476985151750.key 943915 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.6ns 943915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 947312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 947328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3397003476985151750.key 947328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 947437 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_15079567647454715489.key 947437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_15079567647454715489.key 947437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 947437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 950829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_15079567647454715489.key 950829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.4ns