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.624s | 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.480s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.458s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.455s | 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.629s | 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.518s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.548s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.490s | 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.469s | 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.477s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.549s | 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.720s | 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.599s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.490s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.526s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.496s | 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.613s | 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.566s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 3.565s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 3.479s | 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.514s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.557s | 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.610s | 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.537s | passed |
Standard output
839268 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 839268 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 839268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 839273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 842683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 842698 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms 842813 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4443396131570989153.key 842813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4443396131570989153.key 842813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.1ns 842813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 846286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 846317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4443396131570989153.key 846317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 846426 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 846426 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 846426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.8ns 846426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 849834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 849881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.14ms 849992 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_91896307679128373.key 849992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_91896307679128373.key 849992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 849992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 853441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_91896307679128373.key 853441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 853557 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13089903672952559759.key 853557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13089903672952559759.key 853557 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.4ns 853557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 856911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13089903672952559759.key 856926 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.5ns 857036 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16969863235807838311.key 857036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16969863235807838311.key 857036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.2ns 857036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 860437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_16969863235807838311.key 860437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 860550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17707484149120238976.key 860550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17707484149120238976.key 860550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.4ns 860550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 863982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17707484149120238976.key 863998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 864107 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_91255004090168347.key 864107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_91255004090168347.key 864107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 452.8ns 864107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 867609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_91255004090168347.key 867609 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 867718 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_378761364705530852.key 867718 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_378761364705530852.key 867718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.7ns 867718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 871145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_378761364705530852.key 871145 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 871256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2328872027276199206.key 871256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2328872027276199206.key 871256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 394ns 871256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 874771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_2328872027276199206.key 874771 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 874880 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 874880 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 874880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 874880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 878249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 878249 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 878360 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11862173665669927525.key 878360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11862173665669927525.key 878360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.9ns 878360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 881702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11862173665669927525.key 881702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 881819 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4580765049123265137.key 881819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4580765049123265137.key 881819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns 881819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 885164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4580765049123265137.key 885164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 885274 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15570727492535378735.key 885274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15570727492535378735.key 885274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.3ns 885274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 888791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_15570727492535378735.key 888791 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 888903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8569951679504302845.key 888903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8569951679504302845.key 888903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.1ns 888903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 892311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8569951679504302845.key 892311 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 892421 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5591241116188051439.key 892421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5591241116188051439.key 892421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.8ns 892421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 895861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5591241116188051439.key 895861 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 895970 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2667089008652619.key 895970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2667089008652619.key 895970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.2ns 895970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 899356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2667089008652619.key 899356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 899460 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2597768141979553475.key 899460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2597768141979553475.key 899460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.4ns 899460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 902819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2597768141979553475.key 902819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 902929 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4842598371869856606.key 902929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4842598371869856606.key 902929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 902929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 906296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4842598371869856606.key 906296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 906406 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15601856213213812078.key 906406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15601856213213812078.key 906406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.5ns 906406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 909892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15601856213213812078.key 909892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 910002 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3404026834157624084.key 910002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_3404026834157624084.key 910002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.9ns 910002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 913597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3404026834157624084.key 913612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 913722 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_10762009068567767723.key 913722 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_10762009068567767723.key 913722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.1ns 913722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 917193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 917208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10762009068567767723.key 917208 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 917321 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11189268432904778724.key 917321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11189268432904778724.key 917321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.1ns 917321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 920686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 920701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11189268432904778724.key 920701 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 920811 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_9770232837734413158.key 920811 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_9770232837734413158.key 920811 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.7ns 920811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 924212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 924228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9770232837734413158.key 924228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 924339 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13513528092518061356.key 924339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13513528092518061356.key 924339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 924339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 927706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 927721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_13513528092518061356.key 927721 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns