From f1be5cb0865cfacc07591093e7b5dd0b3ec245dc Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 23 Aug 2024 13:29:00 +0200 Subject: [PATCH] Update Boogie to 3.2.4 (#5709) ### Description - Update Boogie to 3.2.4 ### How has this been tested? - Updated test expect files By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Pipeline/Compilation.cs | 2 +- Source/DafnyDriver/CliCompilation.cs | 2 +- .../Lookup/HoverVerificationTest.cs | 4 +- .../Language/DafnyProgramVerifier.cs | 2 +- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1523 -> 1523 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1545 -> 1545 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1504 -> 1504 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 2052 -> 2052 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1499 -> 1499 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1515 -> 1515 bytes .../binaries/DafnyStandardLibraries.doo | Bin 57166 -> 57211 bytes .../Unicode/UnicodeStringsWithUnicodeChar.dfy | 1 + .../src/Std/Unicode/Utf8EncodingForm.dfy | 9 ++++- .../LitTest/VSI-Benchmarks/b4.dfy.expect | 2 +- .../LitTest/ast/reveal/focus.dfy.expect | 2 +- .../ast/reveal/revealConstants.dfy.expect | 2 +- .../ast/reveal/revealFunctions.dfy.expect | 2 +- .../ast/reveal/revealInBlock.dfy.expect | 2 +- .../LitTest/cli/measure-complexity.dfy.expect | 6 +-- .../09-CounterNoStateMachine.dfy.expect | 2 +- .../10-SequenceInvariant.dfy.expect | 2 +- .../12-MutexLifetime-short.dfy.expect | 2 +- .../LitTest/dafny0/Termination.dfy.expect | 2 +- .../dafny0/Termination.dfy.refresh.expect | 2 +- .../LitTest/dafny1/MoreInduction.dfy.expect | 2 +- .../LitTest/dafny4/ACL2-extractor.dfy.expect | 2 +- .../SoftwareFoundations-Basics.dfy.expect | 2 +- .../git-issues/git-issue-3855.dfy.expect | 2 +- .../hofs/ArrowTypeOptimizations.dfy.expect | 2 +- .../LitTest/lambdas/MatrixAssoc.dfy.expect | 2 +- .../LitTests/LitTest/logger/JsonLogger.dfy | 4 +- .../outOfResourceAndIsolateAssertions.check | 38 +++++++++--------- .../Inputs/progressSecondSequence.check | 19 ++++----- .../verification/isolate-assertions.dfy | 8 ++-- .../vstte2012/BreadthFirstSearch.dfy.expect | 2 +- .../LitTest/vstte2012/Tree.dfy.expect | 2 +- customBoogie.patch | 2 +- docs/DafnyRef/Options.txt | 4 ++ docs/DafnyRef/Statements.8b.expect | 2 +- 40 files changed, 70 insertions(+), 71 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index e4bf8fe0ea7..5899a78c19a 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 266c5ee30f8..82a0c1734ee 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -575,7 +575,7 @@ public static VcOutcome GetOutcome(SolverOutcome outcome) { case SolverOutcome.Undetermined: return VcOutcome.Inconclusive; case SolverOutcome.Bounded: - return VcOutcome.ReachedBound; + return VcOutcome.Correct; default: throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null); } diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 1e3f1cad5a3..579cdc1b815 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -189,7 +189,7 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) var runResult = completed.Result; var timeString = runResult.RunTime.ToString("g"); Options.OutputWriter.WriteLine( - $"Verification part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" + + $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" + $", on line {token.line}, " + $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" + $" (time: {timeString}, resource count: {runResult.ResourceCount})"); diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index c10d2dbaa4d..64a9c4bb905 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -138,8 +138,8 @@ await AssertVerificationHoverMatches(documentItem, (0, 36), - Total resource usage: ??? RU - Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches): - - #???/??? with 1 assertion at line ???, ??? RU - - #???/??? with 1 assertion at line ???, ??? RU " + - #???/??? with 1 assertion at line ???, ??? RU + - #???/??? with 1 assertion at line ???, ??? RU" ); } diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 7ae1caf539d..4fbd978f122 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -62,7 +62,7 @@ public async Task> GetVerificationTasksAsync(Ex ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); } - return engine.GetVerificationTasks(boogieProgram); + return await engine.GetVerificationTasks(boogieProgram, cancellationToken); } finally { mutex.Release(); diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index a679c43d9cbf1d0f0d8d7eb91e579ea58f81d5ae..f8a1eafca1cd553f5be82000473f7e7ce84155ef 100644 GIT binary patch delta 47 wcmey&{h6CLz?+#xgn@y9gJDaI_(t9tjLblK^9sg`%pk_(8deK1y`9wt05_%$%K!iX delta 47 wcmey&{h6CLz?+#xgn@y9gCQticq8u&MrI(rc?IJ|W)Nd?4XXv1-p*Ez)J@MdNaVPIh3VAvfazL9qZBQucRyn^vLGl(&H5~~H6KFewY02ay(R{#J2 delta 47 wcmeC=>Ez)J@MdNaVPIh3V2I2Y-pD(Hkr_yDUcvaB8N`@8iPZv3pJlZH0R2S_3jhEB diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index f9cb29a5b534b7f36668cabfa8d9569b0dae5f57..e769ed9dec987421fcaa46b7acb259206608669b 100644 GIT binary patch delta 47 wcmaFB{eYV{z?+#xgn@y9gJD~Y_(t9tjLblK^9sg&%pk_(OjZjpy@b^U051*=bN~PV delta 47 wcmaFB{eYV{z?+#xgn@y9gCQhecq8u&MrI(rc?IJ>W)Nd?CaVRQUczbv02P=FC;$Ke diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 772f901b2cf59f4c8ae1cf3229e4dda346dc595e..2fbac7113ae1f8b8b883e7df831b54a6d0c96ef5 100644 GIT binary patch delta 47 wcmZn>Xc6EI@MdNaVPIh3VAvTWzL9qZBQucRyn^u&D~K_Xc6EI@MdNaVPIh3U7O`v3p{ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 92a410bdb3f91427669ec9adc827c7c94fbcc340..4a3d8097175ee4d49080bfab3018b594f175a47a 100644 GIT binary patch delta 47 wcmaFO{hFIMz?+#xgn@y9gJExs_(t9tjLblK^9sh3%pk_(5>^W^y`I$u05*gT#{d8T delta 47 wcmaFO{hFIMz?+#xgn@y9gCRO!cq8u&MrI(rc?IK1W)Nd?39AK|Ue9U+038ktdjJ3c diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index d959d4ea05e98d7615023ada35325d175a169099..4d0fbaefba8f089d960415d3fa17cfbfe63a809a 100644 GIT binary patch delta 25820 zcmV)8K*qn$z61Nd0}W710|XQR000O8uUr?g4VVEAuUr>dc!2kgHQfLJPJFYo0YrFz z+uEB-b_L)06$>7A?8bOvC#30wq`x$T-q{BThlJf{CY_Jt%L*7AJ9w>xqzUuerzF)y zbz2wPf$ljyb9NKgs!~ZRl}e>jsr-`ceW2)BFY{_n&jY1N zy^pC%fN&LV?0f@CY0^#m;A-5_0uHo);mulIqL^iu4tu$Nyj_52@XdJK6~@RL3Mu22$t2G}*RAaH>_>>qRm`-`j&?oQ+me@7dB z!x!iZB9=t`6FD{TpMende0DK_+;f^FedYkrx7AjY1zRhqGT4|crZafp9;kMIVQJh0 z@GOpgu~6USxn2<;QL<`ufdtA6fmA3EiaFV3w+wJBHtn(4;=IuN^IZs5*C}CyW=|=c z0&c?SQP=V4m>C9fbH7!Q6t;<^PB5bj(0+`dPb{Y3FtT!qxeRp_vy&m-N|uAR(1N2= zv9n7^k^DCzS2ThlaS)1sIv$dLWW>Y_D!||FcP(yE0e>`!2QZqF#weRuoh?_g7@Ik$ ztpICDO+lDfI=f7VlEK6Dw0AMi@oBjbmy0-Aje~RWX09<%gjs6lfe{bB&WnllgiSnE zU9p$q^)Btt1ZBnS->-HOgc`m*WWUXq~8Kt~1?eop5;<6(#+aU|35-J@va>>>!t# zTz%AoVrJNs;>Ld;m}}9_Ote9SrlB$|iZpT|qdo4-F(>ELYRUa2vKtdC$8{gB^8wXo z4aEJ}KycWxQK&Hj-<8FGRah4oke$$gXw&3WcOBOsQZp$&d8)`2Lxoopeg98mv{i|7G0G?vs;t#I#2_bjcu}h5s z$of7>8gG;T^+WRZay9wke}6i3ZLRFZU)AMCLWij@-4dCiz5NQpcCaot$JxTY;T;RU>~eQ56Kkrz_& z)Y=ycF%ui}JUsF6liHI#Mk#!1_Icsjk3ECOBmgbkBf29JV7%Pmi9f;vwdSM;Kx_@irI)4sx7&R5+#k?7MW)3dXSyoY!nDZJmXKosLv zd=sGnLOLBHAQ;n08g>niwF<>p;la!H?yG%-O=tN0BBj{LjNvf%L$;Zq*2%C1 zco6!cNL4@w<7<PuyI(mted(?w^o1+{iKYTaoDm*my2i$aFNA^>7)tKg-fx1= z3JmeAkV9g{s_TUDM9hSmp76cdY&zq<^)H*lQP%5!kJFda$#^tLd$ZlyD1R?RV>I|` z=G-rWcZWHoe}R`kfWwf0dm={l5Ffb6+OK-Eo@g~24Ok`MA9^^G!Ta8fyooETE3kON zXta`*4*${RKi2q!7R*>Vl}rZql8m` zILJU>&TdOe+AQKM+FV0tC`5kjl9q-&+8M?U4h%zA^5Vr~o{KW!z4YG_TV6b!Mk5}#XYh5%oLO@DDF1nuJVbabWK zTZ~fD7UR)l96MwZ0&^JU3aOb0W0ypKETz3Efr1L5mVxQ>AL%tNnUeGm>UU_mz;Qjo z`55b9Fda`PIBhk|_NCwHGr?fh;i>q$KrNh$b$U9qHNoWK%!j#mb*@0BSLX!~QyW+| zdN-*6{^bQc*{*t+;ID#C&PJ1q%m<4pp@rU{5+J>W%y2#k0$M;&P}`|d5NObU!&e1p zj6c~ph&35jEeEq%ARhv3*?J`1je*j3Ol5u;K!qJ&t$H=pq}gc*Vr`)bDA|;=`78~x z*^*gWCOEn@toXOz!F~=;ZV-6zl={q@7xDof$2X?^4+1ou&3nMLW`Sz0q%kx^GH-}b z4dOGn?j$>gO}{$~9%zV7g8+elTZe+q#CO>ll5BS+K0;T>m{3PtJt)=SECSZrMI!pM z(dt}t2#F0ep~=OXu-T@jqtk@A&6-H|<43{0KojH`Ye5_&+hR5|I`^!X58jhY4Nt4(5WjY-<`hKmxRZHwt7Y)Y}n2^4!XIh~G&C=3#ZOC=ljf_JHg)*20xsLLiB=}R@t#Bmu=&MVTWTqa*a zEU|v#cgF{Qe3E?KiV`7N6D2|lTa*aZUI|`RBJ7c}esUr@m587ri_$>SA0Y`MSFy7` z>&+@|pkB>Hvsn%vmynlMYu>jnrnB?+qwMVMYdI3q(Cn)km8{M4;cDE}gwLGO6o}1XZ0om}3gIfzU*lR&qO`32+Z~i!lsF7k}9tO@C|tcg*flHyIo|My)Q-b%y|1B^-xE-h>uXt z!Ve|c9Da^|N8;~)s$p=RbvU={v38ZHuEVEJq)7pr;Qdh15YUS;Yn49U4}GJCcWj5k zYB*Q*@d@<>AH_exAaGe#(6_it2;Q8$qFz)TPU4Lk-!rCia zw?D{4b?}dC27JhrBM`>&i)wQ8`psTT19-Ok{BTc(1&9WJyLp2|d?nW|RnG!=BL@Hc z9CKamWrN;%+SzCfro)sZ6An5$8?e!I&J)nju95VBG~itO&C#>Y#*_D{&`v{y*=+xs z<_ELJy(iO)@o=(|!-ZH;o`{+cIve-Q28jIE|J?hpw@16bJl}iU*#KYg8^p$P)3=!m z*P`oa`m!f~DuX${8Ekl{_U}ZaJ$Y_KGraG)9-LI#$1JL84>QM>58uTZoI>=jM$@ye zJYP@B2sQD&l)@!x#gw39Bsy<~=O;8xJ3@ZHRH#6G$egel`8vV6!8E+Co4y zCrZ*YhTmd(Gf8Rek>yN!ASrimmdl5y@X&$3yDMvdQ6#o6Y3v+R)});hejCw` zl?@i)4ScK-cwLY1kZMq7HWYP_u_c}dto;7_is6m*9KorCD{4_s_w59rN%Bna4WfE! zQtak?2ZuTeg-6rieE|%cQ+)%h6MPwUfLL6(NSN*)o9^YOP`5-Lb_6rd>8qQx+Xf1C zEK}BhnDZ2D2f}{Wk#@V+m_}(b97vqi9L29&mH@R3HcDC`s_y;pgh9EG4TfqG(vyEFi?sx5uWCdK z;OCt?{N%cqy~$74x^R3gSDi;{(GiQF^17k^sxwi^TSaw?n*G`9>eKyS_m2)?vUtbd)_SVyzu15I2CJ`s zJkV9r7eDI8me_F|eT=mhRggg$`I8tJYFjln4P4pnr+NHEOhReR2wBa!J z=Y~L1J~Q}WLSjDgWl#F7EZNfs3x%;0PtyV1Hneg7mxPB$4}$iKvsOYU3~(L-G=0d- zVm=``0+yKuQYKQNOT<^wVxlo=2Rvkd1ihe0UX@-Rby(T>7o5Q`pH(Z7!yq7|f5;4x z>W=yVG$WnZ6gNaefnC$<8Bdg$yNPuQ6rE2$15MjdDgzCL6-#Q2XhsymEQz6#{D4MG z2W$y|k7w7!aM9TVSy*u7W{o^McngnxgA`B8igB_<;3G!+D3#X!D97^>idC0??Mp^d z<6|qi44^1IkrsmbNF#0>g;6v(9;Tn#_PfACeik8?bb%jUZ4=|B*)(kD&6fHSI|#8* zRp%jbOnDH}ocL8j&L8OFLFRbfu@59ZWYX!Qjv}PEuL*HyzI#Vnv8Ie24xdjr4e-0H z#M=c=Eb!VX6FS@ixDeGh4o&KRDq%o7&`>Y2uO2kz>F3abCmtAG575|G51RVMp@mLF za0Lcn=A#EoehN${?c!EKAYI)xWI#{f-1B~W5pTA0!CT3E-+_?(WIM65J%6f`PrA@E z@qGHOhw*L+95blEx3(_!TL`t9&g|M)6u_J!X6@IM#~ZzEhT?{wF~P-WBa^v z>w0_CH{*Q(KTpK>Zuo{YY`{$bdbKU;=(Ehn$|NPPZ`N;nH zll`-2|Log82lmgQ{WG6lxIRl1; z>&~!Y;X`Nebnm}}dVdn?{b{K8y-@GZyxvdf5{+`nOUGI`Hgx&Xq2yaCQowd(DD$ZW zyu+l@tb886)-6Hd6cro*Rl^?r#d3 z^0)A#$t&+puC4lSvrjD8-D_uWd({mMvrCocP*ahI-%b7*F!kVqoh(3$B*--ut#OZ6 z0MxL?JsU)T!%YW&h^~^*7GHzfOzy#36ZwpT4Pw-0^PPv!@!(@6YDYg*f zW67b&qO%Loq0>p;6H}xI532M;!E}-)LzomcC@u&VM(RT%zF1ATu<#c9lk*Gc46mdO zr*NlqnkT1XY62R`TK7SJl+)F(bY?+h0>=T$Vh;gZB>Ss>_%bGIsNJ%o)1;3Xl+dkk zZv_VAxDSd67!AiwP=>ySd(g>Nh<)o#|pYehK3gCK5d2K2Mrzz;#J%A~rV8aJYs zn^rO!UYWfYUAP;f<#%v@ksqACNYAFTYtmCk)9Lfx>|NRzQ3_E}O4J;17LE}oSCj+S z&hU#nVLYsDM&&6a6V0d7WDK=Pbtq%>;1t{|qd+WNfMgDrDiK&wO)8}2j-Eeqaz}Rm zXh#g6S{2)}^r#gW<{b?vyt#{l3N4sBq4ipBCfL1ypS>5aj{Y}HAJ{<%7L$jPUhtOQ z)`K^{Jm34zHwQ<1e!Z37@0p7`rp>Fp*ZT)g1J&E1+99}UsN$1@=LatXl{dqcU%c22 zRBnYTKmX%~200#_hUF*VgRQTsl`mfHa`EyOlycfC#V6&ewj!;HuTX#(R$qhYlqi+SVFfN5t z^#1J2>Cvn=68qS96lnGMPzb(!EacN;JNRnH>l+q;8*44dZdmUbE(bC`TiuDFRM10A z33x+ESMFE`5ij37e=dU#X%9T%SK2Q4k8${ahq>$qp%50VoVS=o0jB|27)W6OJLOG! zQN*$s6;1nDN&Bx(``1qUv5fV9j6*mMVIbB*2Zur!Cm}2>7);6Xre@S&%F)o^H-=s{UFDy?KfE zWp$|yjxK2tBsy}vF^8!+X79CnR}1rf0r&nP_AiSX@_|kK8Mr5g>$tY9Wh3Q(!+3oE zse%_a0VKy1 zGd7#`6!7}@nz2@ewPkKPzl)*<9JpW43I1Nj zDKcAoh{!?y!FY$v4LEZ@SrmtErHW$z_NX2Ja57j642?k07jak=SKi-L&z^s3P{~&G^0#}lMApnhxQ2oLrU0g_k4&N6edOomvO4Rcv-pv6)DJ&WBKtV4or-;EDpd$T5uXkqnxU;R@TF z%tk+Jx$ZGhxryPJ)Ap-gmQmIR9g1KA3mBY#`Y+v{1*41JvlWH{KoY3czXrlPSg8V%pdhue{6(TSh3xr6tu!V@5OYw+SCP?NH z4kJb~(e#5rJn1F7k`GIY%=4k;=Ta=jcA%o!zgjeqTSwFma7(_MLgck<+R2^MEKVrm zM#wUH(O8_DT$yXc&}s)#7SZ}2dq;Cp3oWC0P5d-}mXcB{Ubie3*N>)E&C#CsodA_0 zautjvhU6-cONz-gR4yebSAknfRIUP6AuP900PHwiTn~C<9#PNww1iJoGo9*el*N&@ zu%_3D?OiM|HyYFR?V?wwP6w)Kt9N6x3UE~H7!cxtvAh$r!O ze7YHbX@6{&Sz#47NnoQG+#!4E7HRJ%LlGdi7KP_Et(&Npyk&#+yj2NWq*HvK7H4K;8~44R8)o7pvj@i7iC3-{S4oa z6AJ}zuG+ZCDxBUVU^phXq05`eP%rS*bCN*x5JV`g3p+?q-EuEXt|Tl_G?1aL;?-nN z5*EB@?B_~s$P`!RmNC1jY7O_j-+%x8-n}NjvFd&QU44HP`rKDvJHghc`txe&^F)7t zUJHGmY1BerbM+PFy@3~*A17;M!g{qY?!g5vXLicHoOOxRRC8{f#)jPZd6W(bjk(lk zsGIEhf03UC?|s73Zth_EF0Sy6PkrBWTTy}V)qPOs9;@lizx7$AN1|Qd9d+)hmP4rJ zb_?)sH2H-hC?0r&!Padf3y*{-+(Su!P%ZB#-d86-5juJfCgW?YsC+t>TM3RU@DyJu zRXZSVB5+Yv^vmHl=1FrI=z_nqqFpc(Mz11$+WjTT zwP()GM^?gPR}^G1m!Qm-Y3>s9d|{4IE0JZWl4A=*HsqZ;md;g6ic=JE2S!?aUDfid zI1ZJ-%=?&LN8BlR)FD2h{q1;Epp`S@HWAlLEAyMN;iscXBTLUWRe~t?cBX~fP83*jy1IvB&&Dj3?9$ z*dFKNztE^S`>5r(a6J}*kvba~PD1p!Ne{z+gj97lSpC7l z;k`=!1#|Xh0f2?*UNfLHFmcemQV#?xEO9Qd!V7^U< z*cSVi?yXk2gIjsO9oXj5-u}tOEOYOY)qOkKVJz(Di*lkpze?aS?kfnU#~M6rN$h$x zDX(Ot(m+hQXYe2wA=|Wn9$#jWtuPZ202snQHwKV3kD3VGaSkgr%lU7aN1`f^pM}Z| z%uYAR*h>ofB`&w;c{^>}4V&hHMc0A5-MnH@tIrAhbC3 z-N0Cg*GjDY>p}2(_-hz6y?Ls9Tj=jQZGXKxZMI}sWS&z|bgrqT0EJopP?Mia`|F*Z zz)W}xt1Zo$OdIF@^d0#-A*$wF7-qTonNEi4hpm+9c#mc{g%qL71aAeT@ANixn*g%k zaOu?i3OQ_%O$Z);<~x8T7~2S%ecp3F3)rMKGkDi-zzp$I{hkgzro(iNHOC}#F57}H zmu=A<`$s^xbhF=y3fNFVEPg*cm1M}r9l!-*NJzP13+c-ghMq`)`uVe_y-D@E~6hi_GKlgsHZsz&*rAQsbrecZ<|-_t64DvNN8joRP-0> zbw_@}Uq!qx;(3KJhBZSY0-;g`V_Cucpn*9!t$_(kCL98RFIOg>1XyEVJ_tKi#-NbA z`h=CR*rl_7rfpXn4b+&L_Bn7^pzo-Zxj@63>lG%41l6S@%8UD>w{md(lIvC&u)Lno zwCu@pQrZoWBelFlKm%nB3|&0mlv^8m*sRiA$jMGJ9EMU#VeZW4Th09Xy$c=D>vQ(y-Tfs_LOC>Gv~j;mTe^!EgBOwmPI0@ zw1zTVDvUSr@qxB4!Xh*WV9-7f5>LNtz;lCiFr_mOqCdE977HT3MQAe-(ggVMz7**Y z>;aFpe{P5+bknj|6cx-!ypJofKG-k@Vvu9Ixdn7nT|A8wX_p$roMi>=AjGB63_>8p zk}?{9Ez`FimDItaw7O`z6cd6z&1OQS=|@y=Gq$y@BvCVrDaR@9&26!RLj_=^#D36G z5O@M?&4*RY461P8$eN*fKAnDqO=J!M9Jo`fYLA*%(ai{TA8vRyC#kGGT4XKcwq@9c z#!eASEY#ma6qr%}I68+jEsqyOXbdnmc3p9Apv1_U0aDa!0;i?&(e%m^b z?_mrWYn}+jFfd#|`Teq)fd`nLr~4Y1G+O7V*;8HjuygcKUy)g-JB&@gVyI?9uBLLgdb)-fmOriF93$?Ja|*QUam z%pMO6I~5ck@2cA!%)+vv+_Rww(?_+jA<~$I3^mmk^2f4nIhTD7+uX%ZLGGe3xJ@c? zlUFyHTl^)SFSm$C!(D2l{Bo9G#S0im$&lzWEQMdCK*o&dbm!>v2(y!4^o87FzN&kc zMX)y++6Y=>BV&U_|7z@`v=o0ykVA_WB%7T1WXZtZn+&7;iSqJmNCl}d(rPa#1n2lR zJ&$W^Fi%#csA38y!(@3x0I_};AW)!n1zj1b-9#YS`*e}A(-Qpl8^tD)9wQIJru_7l z3hi4+=hFN^V}XR5YB!vljC>8!*Bm?YBg@j`qIG!Dk71Tw^x@oERS19L2X%ZDb(=;Y z2D6nkyog>1!T~XedxYoStDc<>KNuL2=>*qnI9 zmOxh~kf}GeFtCiNq4Bfg`xG$KgB+gIiN$PKZ8( z9hywOqRvDN{z}u@^D%#=p+4J=Ju4V_B^Zp%l4ACKP8eC0v5T1rnAW6uTmqHQN<8-6 z8vhzG2HrqRWQ@a0^I$uCWHH6D!0SR|86MM0W?mxc@udt$6yJD^nkdg?X{M+&*@=Hr$Qu>_yP5D*)y&Vr zaDnQ!GPjb5kIk?9(7U+@p%HFKx4=w?zm{uZN}VVWGxtt2JVJJdl4=B;aC|&LS%(KWwB-h|pFT zAxdMeqLvB}Dh^fR=>FUoRFbp*zoPY)9Jyw)$@7CT(&-hV*9zm-r0hJIo?jnL8^aVF zC78%fT_=;-NO)jJHO`SALXVg8v^FRM=uJk~*KHhB=)znYosQr=<}`Do%bZFUC|g18?o=+wge>>m;QX3IG%Za+7QN6-3pON9=F?C=%UT% zz?UBqST(VKa3?d752ef~v08tdjq-G<*MQxdy+VnNChYA3{M`_m=5jQJ9I^PjmFNI+ z=Q5-Y7h81v%M)l`(NDds-W$tCu@JwTc#V|*0L_Q@hI4C44LPw<(iI(4Qg}@ z;50JPoXb^N)J;I`xI4E)#nRp3@XcDc(KBP*XQm|EF0&cXgNeu}d?3@QXnF1l?WCiK zxdLG$#*lNp=>gR^(=uMs!u;H}omawdPZ zHKmat&s_cFk#e<{UD3;h)nnm8I_05c|#_YTg-k>#^mP;apnJ{ zvnjB!z58lEc(SRVl)>~^JPET}4nkRpbZQjmM6r*K9DQ{H-d>TZx0?KbQGS2cui3PZ z(yJUQ@f)lZB|>7XtL~1+(}9nwE!`oEnZ$cI+kuKooZC7DUc9cVr3BrgSQAX5&dB9V zN4XBtDx`Pnk=jb!`DoKCyRMBIz>U#(*WiQ zj8ym$YAdz5jrIpmpj=)VF;r?RGsufs&0mvIc+1_qpCKI6V?$cD$v{X=dU!p_dsl5I z%ei3=E9BiS&CejSvK8qq-ft)(4wpoVXA)GXQyVa|iG?thSRcfagKe zq4xAXc2lv5xD<5mVXM7O9CP%Yt2Dea|@z;o^=lM#_DNe?(K(5 z&w^rWICeoOZO6F8Qr1G%=7EYD$_}f@b(_rAYKOhWTR~Koi9l5Bh_>OuT)denkF|u^ zD}#(^G^Nzt@FO3wA5n+1I^u|GyDt-~&?O`J@Wf0&>~()Pfl1PI`ugDxEp;~ch0L|} z(DeFZ@7^2a`nH37MN0tgo!OTj4qolOWQXYTk+tUshkKj)bxqILyf;qI(n)@Z({M96 zlD~C0jICtlSAQA&kik33jO5TVsDS$`U^w|K0BtY6_%Rawdx8UV8aRit3C-C0D#B

X4wHJSjiGXwEW$)GQ>)oS+*YcJzysX+XFRQYOa#4CRo@Vge>!W$j*P)oj4M(YV~CPg(_&cMlXz6$msEQ zqA;pU+lfN21-ns}aRKyJ{aq=FZzZx&z?ViB_FIiG)V=j7(?SQG!(Evy5Su>5i5Rk3 z#TddN^%!5(pb9~O6O{&}0(>aMvK`wrHWS8I;QC#`>Cvn=8jmLL)Z7F-+PT*N@Qkr~ z5VC)#2c9|2kKM5so=XzI5B$lJ@m0VqKR|8>8-iO4C%#VzlV_4S)ID%$Peg1B@+U? zVz3YYYb`Vzbvues0?+W_n{}jg_cJk_r-OfyFqbdWMkyj;anoqDim<3h@BDlXjGJ3o zZ^pQ&lcd>LD4|<)^vbC5I9~~yTN&aqY+DsL*D6AFxtv>Y7#$->=(Id+e-uD*9(Am$ z7gh7@ylAbYI0Sf2MXon$rCfD3C{*rkQz|Z$P)RR?svMpq3i^%c6>D5Q5&B9o_{e{1 zR%uTZUjgxLj!LT^G%a5I0y`)Z6PyMI6oJmSm`hhtD)!JR+>DUo44xxp>9^H8EI&!S{=4r zO!$^kAs*RT>d)%A`x4aZ(@PyMfKn+&^WqdYAsEb%=@2JIDuq&rAzP#t4{XTAD}M26 z9wDaX;<>agP7XGF{4gPo72vJo^VOUkED$jni1hJM>=yQmVXjCaWSrSN|%orjig z4a{t)`)Vc(!&yE`GwvyR`+PJ>dou;7W$EaU1s9x*p8rXMix`1kgR*Yf{PucrR+ciX zzk0&un4a?(2hKWH&o~IKTe=C{_ze&mv72SCs<-dcS^Bl2ov{_BzY5(&sN*2b0c9xz z5l|h>esW%}E9}1D#k<%Nx)^`rMIuU&i?%w^1MaVpum;*2J?~}tpJP{Ke2RbXivDuD zqOfCk#dvnV`3|Un#R#f0lPm9xXj@c!M5+}(zYFio!PcJE@Y#U|5_o7Q`e|nJ@N0T{P%ADw6T!(+#Rz}EWt9Xn1 zyq$~xFQ1x78Vw!w3aPebG%G!)wTg^aNB&lFKD;o7y%zW;sk^OsC@pr=SY|(SM9mQr zWo*D>);g$>AySJ4i}x`P`D}S|q&6y?&qrCFL8R)H3N#QF*(iEnStg~?2^?;&vKvQ& zud-uZq1`r>?vZ3*xaEAIq(3Yk zEK);b8~m=a9O+soZmsNC{l&5ZLB14OYSJT|L?C%4Z2+LqJZN)zKqEF@kk!7O`n4u8 zHb%7xng@JQ+mjQQe6t`lbi)>hA8@Luf6Kb6F9#>i@)@2QE+j8aQhCexyi--+bpm!7 zSk3n`J0=w?xg38)_uScB*3ilq^pRY0=pSS~o5SuoRu$d9#aq@?{9fDY?hUKy;=Te!yuTk7B#VSz>N@3rmkwe8QdwtaP6 z_w1yseBFv3rWQ+RcuEA_ndPER1oYKr8fXaI8o-5>EvYLG3A%m7?YgmP1} zATEPK`=o;hHN{R4YB?fJwDX*o91EOxo>5rQM`2dFU= z)A1gc(HZKFN6|WNZw(G#VfK63kbGkb3c1U|<~>^Rs66of?Fv&;BY7T}oW9mDij=NE zhL}V)k|v_jC6YkpL@N);j;g2WXdqMTFG6b?LY(cnMxJv zIh-KDd=K?fIb*_tH>GQ2QE+ZklR!lh0r-FOCYlBSDp{!jq$n0bwq{%uG;Jn1Y%|{z zX4#R>Zs`l+LW!VzvL$ih=?~nKt;9qsJa*f=FDj}`e>?&A=rm_(A?RU8IZ$n$FCvs; zVyEflHKY6nd{WVqeFCohO%LK7JmYWNy-s_B_kyH@XI3R;PNFTD;;(erO8VCOc=3N) zL0HN(RTbZ6pP~>Wbvaz;AyN)Tk-VIgMPD%+M#Eec&f0*CcHW@Ad`0%X>L9?8sC&pev*hS+Ld_rj9LGlwK21iFx8G4#XlPnh7gUfVw zI-Y(O6r()3+Pt3?J!Uyi@}gxfwUH))EJIaRWtyVS>cP_JR@G*d^r=EF2cCafYC)a! zZzBScd@wDU8;H-}flS0D&-vvSNUn|#rG6=RcU4aRY5xOE-xZwxl&Cjr%Y?mv9NS)E z5EAXCE}>tQ5WuAORWS%EWxyqY){`-Q*_QFZ?2)kW&E#}C9^xn2(WUJp z6^C65S))!&Iwf^bL}PGVJ_dii+02XqW}-e z@lvvXxjZg>ELk!+%Ndg?eKolaChsWl(Gbhh(#a&(%?iZ3%(D*j7KEy1cEOXF`cbjM zuKc?)bN3Ut6iJFR&^xW+I^F+*-7vuO!{s6oXA5=3a~7ILMZ@N_bB}+$!kH%Ru?mZN zUM}f_EH{$=1oCC|#QNS=e<6}buixwiWgZi~3kdT_JoJAGn#Xw!8amr5oD=nXopVOG z9evCBp!;6#Y(TRbz%C1_fW=;4S_(*zfMvltT`EIs%EqY%9=Plh?G0Z|8Mt>HLGjV?Qg~QKUuM%2>h+t z{?=?!%{Ez%W_$VO`SYM+g9mz+rP#Vsu|a3WdaZu1bBeCp(YMrVy6^vadJQCC`D$$$ z46P{}e=W6EkD{XaxPV%7U~#qPYOcw}nbBPI`d8MLuYl>$3(J31Wu6GTHD8rRs<1sF z5^+{ZESKZ0iX1Q4em&pUY=`zZK4v>~=bXjuM104qp6~d4hJg!>b0;BFq(JX2;TV&0($9SHg1W;d#_ccA46ck}?o zy6~W&Rc-7{S!wdDNs~uGtCUJR(`W1D>9oIzG}L?-#Fhp*ks`7{Uw@enuh}WS8h84| z&Oc>OBQElD6*qkL%ns4|S{zNWVu_)}lT$`P9! zbsb_0g1{!;)2VLtjKt(@Krt1jo*T%NOdGz&9u z{7HwksIibH=U_U?A@J3l1gbfp9|%)b%xhP&KtFV)YR-b)1kCDxNfseq8vN{2;1#i@ zMO`k(f_VN!*Fwb-kM&SXiBmmfs?~pwDqzS+doO>obUhut8)0~J(QA=ItW^88$j}*0Si8=ak@!mKS&w>9U2q^|m8 zRhf}&zGU1hFwfkp`#R}Y2tlsG)fc_%e){->*hAF`=(U+D8tbd22oJVo(kKvUgrB%H zuUiIro(9BguW%gF;2^NYU*>3JOT04{>h^!7%9fL^G@*0-dvC><8ZeRKi0p45!g_ zSUm3S!Z9WY3lH=nql27QlvErYT71o2F#pXiTuhv$1;OjG5hlYEO8b(Uub_) z+Y7-2QSldM?6T}pZe3eI329gYQrHr(<=p_JS~A76n_XE87=o^@kE*=K#l6#!6@%|8 zq^p|PkmLBlKZsb4c+vX+SK)UsywfQO4^|jVTY6Rc@+l8V=A>zHx}izVs^D$UM#u$GKp;!F}~&Sy&&65wWB8M@T%-lDt#VTX^Y7<^+K+h zms_`{$^peSpuzFm7X)wen} zlMg+-S>a4eWUEOKfp;_tvtoandm`SfobBh3$#gqu3`KV%@q?Y>4wJ`;Xr&DtsM{F2 z#zbv&oVtiY*u=1pSxv*YFQ&8e_oM9W?Q4|_D%P!nZ&Yt7(8{oMl!yJuX;p@76}AYW z&2RizIMmw8t2;*X%r%n8Z0;2T=1{A3|-;aR&7t={1UG(a!dx@j=pA6P&n=r@>_0 zM7XGNslLivo%SA9b?Zy~$I1s(e40S7p@tvle2?Wahz0f%zGGUx5%nIFDcp!E1_=ss z$!_@L5>5BZYI{!&L+yV)FXz~M%44>Vkr!tbVw#oO*vFnP%Q~*!^~d79+sDwxtqfB& zq6Ki>Do$`~fWUe?B}Qc6bzu+bmWR;%{Z$&zmP>8RB6g9zS7_0;_g?dx$6EG_E#&Y@ zek*n}O!JQ=w`D(;Cg0K(t6Z0iC)k2vW`i8at)VBpy}QAdk?? z*z^7 z46HCQ1eq$LbaH=WtCwI}ZT&K%N8o@p<^8UA$q1fr!m2*C=ao`Q0$oVpT` zxUXROz~^yA#JV?W0ri@vwtOtK!BgM!&Vw~~X4{NPkfgy~GBzQMq0JmQcIlsid& zcfz3i)D0~V4hxT_nu)Ds0iz^b+n8ozE5R7W_&Ua?#sYk$m)0ap#Ym1$;UWuwve-6; zcf&Z_pa9vXo<4ZIjjiNGpyI|*QLtOX2=cwGy>2bXZ8{!*HoOl$AQ_ZMfP{*9-OiuFsY!PcS8Mr7V7UeY-_XX^DLGv&~S+r z1Ur-8m3$J4sykpT{Y9}e)sc~;nk%hg?223m-G&VW^lH1Gp2DV37cr~y1D$D$e|o2^ znLS37m%pKZAvN1a@6(Cs$=q)HfH4@KXU!(7jUb~;EXqN5xv4Ks%EXg4j~C^s?1dVd zn}e6FWL>kFGNE4HAuA$-pzHCtF=0tVX)-Z=CrLMU{pXo!j<@Ff6`J>h&3W>t00{G0 z@ygsTwoM?zpTeyUjIIWI*$x5bJC!h>dGoUUAJzSTd8^gMFXK7Y4f9-nE8uygr^R^AjOY;0&F7`^T%|#5hX9w8 z#G9A#oa%;oF25D=4YQj*6>vM;O>Jg# zbsk)Q3yt>POyt?!vX?xzemJWhs`gdA?%9ix_}CtQYVx1z5|>pt`=l58A}YUUwQOe6pl_Y$_~QGOrC#ynnHfTh$rWhvnq>P81dBPC7`YVkVY*#NMVR0p%0e58E#+dc8HOjmCmX z$HHe$foLofhhU^dSqExwuP@M$3|fF=z-(MJD7bQ?=U(+utHUuDTg4~4>x$g*fXQWR zz6IZhZzH9kFU#aw7GLLDHyX>JWGOR$>ANj^fnW>Q&tqQL?Uo=IXcE{^7x6fH3r6g?x5x`w?1@|O5SU4$a|nzwXAXgX>GZ!7 zh;6!v`E9pY!!9%|bUAfuJGGT#sKYy2V;u!Nk^+;34;)m#UEVJ-W{rw0Rp19f1U%t1 zLTi42z*>dIYtZ_e(rhri-ELhUV7CG{x{MpQBx+U2Uor+uXJu!}5SLA_hi>`EcbJ~5 zsGSxb$v^$k@^=c(`2Numa|JAa_|o;#4N&qdv1LfmU&hxLIgP1~^|wF0x;2i@&5B|v z>wW_%^G?qy9zO53( zgu^WL-3n8Z^B?wQ3Oe(*3EP`w)o8P*@tC7Uad9dcs#UJ<7GB;p_iAH*mv+t0Wzh?} zMK@|gcvQGaJMS%8)180qwCc^-IE=6U{-uoQt%7w922vt{Z{=RZuRn)#*PdS7}v{WFmpfegJD#{!DWh*ErRi)8ShQ)ti3o!c|x;g#@zb z0uftLZf)%>Um8M7YFCS_#1R^h$~HhgYn1%A>jY;n&Qf98_pV0Mv#$aHyND=-d(wq1{ZX}`jJh`~jp6pKK;AQCtS zTmyx*di#7dNqaNXNeIdoQ_eJ(&S&XxBw(aE%@x#F<`VgS9v|&Mt^=9l0L(o(v5v%) z%0%_e+c_8Z0-|kE#sGCqZIw7G(GMZ5TM)*Z%CRg7j z0YYg}Pk2Lr4eNs~J4|kXl*UM^zREnheeM|JTPh_*iqK6KS3oT(gE2aqiWeDSM;NIt z8Ji+HH{!fv-F*Xw6e;cy<%KjawsJDCfkYjhmMgEPa;Pe*YGtt%5d|t6|4<4$K%oB03d%WRmpNl~boVi0#rlD4QLP~8j5!~!6D^kse_BFlTJHe164-torD?#~%H&Rz^I zVT)W0(W>TCp^7uq&KFNo2~kUul1gn#yPtnds*lQTi<%#agXJL;#s*O|Dl|K{7nz+w zv`Qs^DhPTmB4Q1+C&RL?{fesZWfL+_--ftyTR+_UtrG~_yE=sM>4Q3;I?Oo{wooBm z>27>%KZ|l?7+(vsThYV41n+?)OjtWaDS8e>cgwIpi`_O0o1sCEL0J6!QQYz*pvX^P zjYqMU0IE{0rTYkwm8Bj6taVHNfqmvGE_G2Z~f;GO~HvWwr!cbu7VXRb+s8uwJf z_*C+``p&RBCQiWw0h^Nm<(U$n6ge{X-d=4dlpQdsS4s;++t@ZwF&NBdsiMMLw1amJsuneka z?Y#XldNS&qeL`jVoI>EBl=1*VolEw;&ML}r3PfGW(@lnjIpI{b84^uvM?K#;twASt z)*8g76+nhdI@@obCTHyoQ}Va%P(z9(^hQ9|&1xSPc+YQ$@ax6$Ke*Z6)hRGQ;hlzY+7vO>KiK-{h z)wx|+R4ehNpr2~z>!_?rt67WdnT*n@tew$d z@apLs(Jt9epif~hrH9v(ym!@qhEk`J*%pMWoA0b)_&MeH3p>t}z3C_HYdlU-IJ34W z@vH64X46n}_7bz(BQVpv!wh4dwPmSa{oig)e4N>SHseJve~%++42037(c6SK0>lOs z|83%b`Tn^l=0~6JoO|x3xvz$c!(DR#w~|4q1H_<(|MW$bX48k&yQ+_WW8cNG7lK2&O!s$Q|IZTdl*x>oc*rnvDkYbk|C* zBNSdYg=Gzov8b}^A|!Tyg^h4~h{#j>#6bqqUuz@b3bgli6u<1&kmE?)4RcFwax@NN zDX7mcv*H>+x&fkLkAnHew>>^8wFR~UA`E624R?IR`ZE!0LONW0c&?JWLJ+KBaYpRs zrlM2}D`Gl%H@;pXcJrcgH0w>WQ9h?u5q-6iKWa{}Kblb{{t?H2bDHi^t zzV-!1p%oEp_1Un-|K^RLC62K{9}V)k=?IGc5-6!b!K+!i_QtTsRffZokgPehQ4=D2E;dN$3md0db}$nd_r@+pEuqVMaBEJKqQ?vx z7&P%CoJD5}1#Mz~+=&0-2cr*IKMibIXyRnT1Rb6A#-$jZQN0+B@^cB6|M-W6-jxR1 zj1V9{7nAU-*o2C`S2>s8$%-)|)c3h~eP!SmvAcIwjonl)%5M5xkKM8n+FMZ?WTm)H z6}zu=_{()E1;+R52ROFO(W&(OqT@G)75SyF;7GOU>>0j)Yz{|RuRl&-PA6kL2HO>T z#rIpF2 zcB2ALyWh*wRx$xsLdR++DIEwh2RIn{45-7ueK3RfJr?opf0yX`JFtUOv2h1FXb%>r z!-u(_(UoR@!5@0DYvsX8vk(XDO4qXyIhq27ynBJoB;@Lka3+M{)6u(8{zUMmF|etb z2!VMu{Tv+-9JL~15M6YAG|XFFk!tF>8kb;ThfgpJgiSCIDD2pK5ANCJiw}v$Au=d? z*`Rlx{^!LMJX1ER^oNEGOcuRj15w_lmIV6C%J27oRzwfKudIB9e|``2^k$OA`#Lzs zg_(ZuMEg`QBtgM`4o>L>yG>fjJvv6GwnOAzKD$VX@67RV4=<+N3qU7f6Z2I3>q9>t zoTxTc{bWK)(^ O)0I^#v;F_P%u5LWY^ZktcCdug}uH&vp2|-N-7awmqp9Q2$Fsa zoA*0^%JXr$HyMt46EO)?RN!2vwC-wnmANX`{u*QwkY)TJKzUv>}o z8ckGJ_(3^-fgt=-KHSTfa;BY#7xn?Jiw_5X!z2#BWesG6Trr6$TAd#>fE9iLcU0%#253SlGA5D7UVPpoFH(bXEA3_|d)`Lly zo^ZenGn@{ChEuue6yPP3N~jc=)T>c{$$N1zehD6mcX+(Ddy!8YGAwTZx*Z0TrjQl< zXCtv?=z^FLUA>w7K#Rov#Ma83WBM(b$?$?$hwHWEmA2a4@z-p^4t6w!bFj|{ld%A$ z$>|uF5muWMZ>a#FY5Z6mgYCs;=nI=6rspkI%4;Mc-rK_yP2E~+cx;$fs?t(_ILI(4 zEFi-kR~yonRZ|J*{v?I1;V8eB@);qs;S3ofLjTbiDg@*B>0Sk&!6fWou$d9*IoRzEjEe>wCST;e+E_I0uH8(rw!UIJoX`paN|RHSsrBxrJ#<6wR zgN6}1vJ>dV_n>-Kmk9LSq-6|$f6#IUs#}3#ip$dCaeF^W^6T>ydD7V4Zn7fcnlR_V zsDtl2PJKE=m)5kYM0npQD_W>BWtw~*<-$zQk{{GI#I^m6b+5Kn%JX9H37uiR$Z{$t zPZOfiN>W)Qhx<@%hN>(tqL>YatSC(f)16~yQirX?42!`QM~9=T@C&bh$#Z~k<)80I z4X+%g$i3~M-rH7T&f)YdH4^5rNVG@;>=6}6l?ZvTzfd?$K2A0tSXdu-kzh&W7WIp) z=^$(JaZ|&v*q0>20!TxQjdawBb+l@ARJOn?m~TT;3U@w6;AxDBsHS&TY>7)RRe609CopDW8s#mt5mpm6|cfS)2o0xA?R!1 zj)Z^i{ny*4`@ilV9g_Y7g|`Dn=DpQUcWwRQ#*dGF+WqCp)4gZ+SSz{Z-)7C7ugV1g zc`thB$1AINKXtX0taR|Nj`*vKe|5!QYxvii_-h^iS{Hvk#J?VYioZ7SuMP3nkNDS* z;;%>e*CX-QPx#kQ;;$Y-hEDqQC-gF)KcSl;{R#b~^e1$5N`FF6y9UB92Er2q;i-YJ zXCOS25KipLC3CQRQ-6wcT zLt4N3myb|LzpUc*Jt0g&ieNf}Cg^PN_+ReX*`MrYkg+&_9ljd(CTU~DdbX4Jox^ub z;x|fmgvGFdMzZLZmJIqVgvP;64Ll8?CTbh5Z}cy_>)6;F-GPqktc(BYHvb&Gdw+N_ zn@!&dj5&aFhN^_(k10SrhyVEFhi#Mr?6=eiJfD89+P^pIx_fVgt=_$My7NP^lkd$i z_&3~TLx2x|(JeM5=fbe_$p+^dweqo*jXY$V8XqMsC5-R|>%3`E`~yr%sz3|kp{n|<1u_Dq(r;?@S>l|n+mX{)Wzv1*kr1+o;zF-_Axf?1~*5m zz#(8Bm{ zK>CK<%)kH!3$kLTKU-BB>6KVVGR~B3#g%$YkpZM|m_>tCF zQ+MwQr3;*mfb9*{x=~1rwz8cdA8(?`3MaAgR{-V^0zTv@(qI1W?C)%$bQFMW>PgCps(>>-3W&&SEd!DMnD#=$5g@+OwT? z(BtD2c1@v{GJJXCtn1I$R&sOJ!T)w|?y!SlC>81giuJavCiOrL5UuWQ*n2#6_ZCSw z)6dqJVno=!unD(cM13gdZa{T_2HRr0K>#9u-tz6-L>{J!JO{-_zot&x2NOKcL<39< zUm~IyzT}O!NmN`Zgy$0ew%8mM8u^Po-KSAbSrOH{8vCq7lE8Q-pb6 zc4W{@l=bdb76^LLJ8yV?oK|v~%}t2j(mJy)xO>RBjZc?>0KbdLDK$)oHTMZRXV%T7 znAgMU=Se;dYzKftF68q|oQaQOJ z)~n9n>+cMrb{!#JCV5_3HQqyUOWicaOlw!3RUFt72h6{1?+YK{I?Hv|G{+DBR^AwO zFz|2YeE|l>B+%~fZj}zL0|?QNI`h!BLKzU(!xP2LbNtAFC|^N;8Xse+s2h`fOCii$ zR!EHNqJcusJE%HhjnS3x_dF__N8DF&$?V|L>s-&|wBu!m)p8&~AcJ+Ju9g!SY$Z!} zbe-_xv+X$2k)E3}iN{*%6!-W<_ffdcMZ2o#2-=)b=xuu7APO<5Op&0;4(`QBHL>f~*oPz9X+X z8%4}ABy(;FjDzf|H=*OVJ$W*CRtsiJHjCMW?YJ|?Jme0af8+EhW2giOH@OKdc6;U6BLIp2cF zg~VxSyv2No)zWR5l`;OCJt{SRlb=4a06+nc6l({6O*hu71r8H!ay$kXxG-F>Rn+NJ z`8&YulK>W9W-D-LpjRx9WL3YF^f`GK`RQ60uUEJYiuZdKvlL1y(wPrfSWH{gu{vCq zZ9`cvYMB$BoUx|2BWR)nN76bQwHRw#ky2xc6wFwl)ai@vAFeagNITU=$1#|l|a8IWf z{UA8Cd6r8s#nmn?m{vje^3q~pn>Q({FrYX-SnnPbf30bAI+|tqZ_^pNX3bF%T0iF7 zW4cT5&@zFn&l?XPu01ToKF05Q*mo@jN@H_>w+fR4_d6%eDzw9=Oic92(0uF2Z)CE0 zyg}vZAV+}U4NbnfB^6*mH_CvB zs5=a}>f$Z0%j6$PXSKT~uX%M=jefuC=o%aA4?A7F54I{RZZKO=SL?2>bv8O1*2S@h zrs8L;ctJTW@FVlJSOX$={Ym39ADQHT@#92*y#dU;0rOWRT4Zj3(t_b_u~z<2-}apg z7OmnNcGWv)Q}WE4@6tw7aiYd?#y)lBr$)oTgMsg^18$v-)gWi_MU_Uk`_La2VT3@#$dFJ&yQ{T-ALA_^{v^9v zdlcyEr^2q9j(ix(D~LydcB&^K>)%vDyy`JA7uDBpRiF@}u$lAs=G$6C*w!&kM2EH# zF=1Qp_!6+bR#({8*W)eL*Ggr^`OFB6$kcc8tNw+(fDH7S3%XdEgP_;Kpx0f{1ruIC zS&u+p|4#19OKAgCa8QDObaDr!Zr)v8FK$l*8Es$gA*JDR0mN$S5ikuZIZ3Jd(wwAZ zSuNccdSyI;-5=$~^hd`tr!?hN%$EigD!WP}d5k zN9VQS(@&4q`6mBigj=1Tx?)RkUF5CQRRwuB#q4ddCKXuCMZ6w=s|9-vuLCalkbzlg z*Ebil*H_oNoY}0>9|nY2qS5ct=|+6ZiqT*{-iVf!$0Ra*mT^&Y^jfBMg@JUmPrb3M zaG(&f2CHs|?>J$Ya(e#sW9MOK>pKkf1v}RGX=7vck#!i+WfjfoM(5Gm!&O=Hk*v8E zlb&@rQn)BQfUt#sqH$rJKY&MXy&0FlfLKKY&^BS`m%tW-^cOz?!3lEaSXF1fhpnz} zya4Xnd~lg^E<3SVuXAE!>xv~D+7O)EJ+yJ{nqqS?avY#0LhNh?zjNEB^lW85DY=ak zltSC5*f_4mEn9!thbPzOqysDbBUuZbVqCE!7Fo|bIB8seo1@(N2V9+ptF@1~_;g#& z0NK`0iN#dB{aD%%S!>6c%A9%La#e=R|@({Yh zGPipeM?(m-mnwd8}~%Xh+Zl z4s4-(=^j34t4(-2n!4oq?g65Z(uSR`#e{3SZ}z;JP0xFf`CT@A{AQVr#?|^s1`YgK$B5^d;W8Gi^Aq$UM$==RFie`9?nMKmT)XwWlf*M4I4gs6xD3K5s&!a}|$rHrMoj+lO zXbx4IKT^nEgOJsjLLN{hzAw|ydjS1^H-x?iAfc$qd%`;NkBcs?#tA4Te8k6?3Q%K1 z^B>qOr~I7rz1n0CNQE=S?P;hP6q9@*@2ELyP5`9W75$mV-#T)yMqA^<1#KRb zq7)G^Yyi4VVEAO>Yxfp%3Cd2;BexIeW9S0YrFz zYulPimPNn&E0%uPBxA@WfQ*7L4=T=P9~F<_o^vn5lN`4B`Zc3NT9qBNQDBSn3G+0%K*n>(;ka0&I`Ri--Tdxof1Z9_LRaY z;3kY7bsdk6nPCt&_gfW7VVg+m1T(q-?Z*iE#9|5#BP*Af%TPx#I~n4wWHD$9EjTWX|v6+L~ z3b2;c6oh%D)5~-q89Yc&yBDJzpOy=8xrme1I5-1uW*P%Un5AZxjd<{NUQDc~Y~rcv zioF!CuL15@^_RKC@gRO)X~zJSHH{0?>HHauz$;VQU^TpyQNpgVIx@6>njYSWMR_#o zH~8STk~man4$>;uD3b+Ujw8IIb)uG$|EBf0&UB-7!sT65l=NGIVJ!{y)bDb!gIsEI z^-&LsnPF3k8~pooP1FFv& zi2JdD;ILz(P-6ssD2uCqur4qlJD~y5rpc-9I<7yYW>S3eRFNyn%@C(Ux(II*GIhif z*HxGWVfE)JAG4SEZxAT)53T<2quLO1*=C&v2O6OISF^+bJj1@lA6(}XLhiC-ml^|* z^?i~w-X;I*r{vw`O7heHN-zbm;cL_4ssj6Ta()dFJdF@G&HA=~WnjUwwjxclAz|WX zS7l@>f;xA z!4;Tq724cZr+H|9MXS_Ua(6-08P(|6+-xR)IDN%}|E0kTwM(NXTxMP5MKBix3BY*YC-CY$bnGBjFFX z>hdPLp#z(QXyhaxLs8D$N9v?w3PsY3>k*{C>@7!zYv;nZB?EEY2Db% z>X0FThv|@50%C>~R~DYZ?pF>@Pr54!eIW}#qN%_UXM_ituCcM<3!z{IhLStB_nV-z z0z*72N;UO5i_BtCwy-@olLoJ{p;pnn00%9qx98eJQ|ME?sRuL%s&Xx81}!J zIrl{H?l6b+FYpowa2OJBkHx4S;sY01`*nBP6|JVjKC1-$Ll0-t|InS1H*slY2^LQn zjaIVM;XhXSk2U^do&R{ie{Ap{Kl2|C`Hx5X$BBj0(d60i{V=Cvi*t?~`ZO&Jp`>G> z2_>t47OqgTW+4nE>lW5f^1wnJN;WL~q2yYX)%6{uQIeRe+mf0>Rj(w&t8OcV zh7kmXbglIC$fx|twA=qA=EmUhvsQAbhSroy!4MlO@wugD2=GPN^cQDB&@N6-hgYh- z#V93hF&;g}u|p;yFo#jDkeZ1wa!JI0QrepmD5wx>8JIr*kzV7HDM|mReut(D9M>b9 zPq7aAlhI_1(^kW5U;3Rs7YtS%o{GN<)WW$~rzZnj6O1p;e3*Mz=L%$cbzT55wSi^B z_u~rSUtPeH?W%_{{wnC?Y&gEie6W}jTIdZb0n%H@4CjL&pald4wVfITfd)N)d{uzP z=(CN3Sd(GZaxj|)@*%*MtxM9~=qqi zoL3j4QDbZc0~rOVURdnD%r3Xyh}B-)@YDKT{hWBU#ejyj>~{@UXe!SGWi-} ziS-k|J3jE^ljPf0lnBY1C=pWFqC}|nO7N-@VULvclM~UYL<9|4lm?RiC<(H)Jrl|) zu%w6o;`pzI@Hfv^(nfxNGm&njn3azH2u+){=NI;I@-`oiXr;--mWQIPYHZqn6+7#* z?zG|t>h)AKo95tg33+L?=6&~aGClt=%+B7uks~1u&7P`J$=W<0ti(-C_}nS5L^UfL zj`^u^VBSK}6SqV4)&FX3JHfWqx)m)zz621mf0>Z`?EE2IWYejCV1Nx$*dxNV7b6g$ zwppC*`pAT$8XYsB&I4#gP}RAEIi_G62u*}(CASlr0QX?G7{g$6@z>4acyK{;KF_`d z5pcJk=lP1Y|Adl`y(6u%3l(6zZD?tePW>iYi1UuS+eL=i`%)y&jJN+$4|SA__z2}R z{7{n3;TPz4B>t{{7zXEAhjY6gYgdTsI(+IxniQ}J-VYTG0lgTrR_NpX&^Ky$$95>J zgmYCNpHN@$QT!7O0+&@aUg*LRztpQ4@Tbh>EWWx^K{=%bp5Jc)R?rmvZe=^(=t5V(`z; zG1t{z*6*IDosC9+GDt}>;h>|l0UJ%{JOTae8c7dG1J1SI9zE}DJpGUg?KD7`&GxTp zelTs^dpfxo4aQ43T!{-|tFEYj4Cef1u;HQFzY~r2e@V@7Ia8hX>v#6#$%p6-jd>3bM3emk9PR_pZ zd_f_k5No=p3;PhNi0{1(Vhq40thN-G53t;CJb19SA;w)#Aeo^0_2f%~&5i_W3jxub zC`r#4ev9etIHj>imNV&rq}<(UE+3x4LkIruuB=6Wk=VYZv2#pWlXgn{jcgdKW$J}1 z8!W&Z_*f(Gx*p*n)u7C5DC!<#OFR!)`u+DM!yD^4f>Q}s)S{m5+X+CEV?}+U;Ir8l}l_AaPc66u)j+0@O0tC~1MHx(|aB2IWFF7^q21r(Cc} z>eD7@Z5{SL;=hJ@SpH}g%Ef=(@`q6V&@Jw)VEv9)ztdU44=er$?76e%f7rmT-EwEo z%mCtGXj0i_jFob}n=xkNyLzIABFyns&T-v;vHuQbxOIoOHghTP+NgB6SWBSxsz$T` ze%`smPp-S!+x&EG6^^gvs`F4SI${x2URSkzHig0@V2#j{*4`gqLLk}O@lZ;o>_W=d zvJhHpU6Z}f1lA0yfUCKwIun(=RaCdA*`K|xKHL9w|L71Vi+Aj8t*5H~%l%hxvHH?~ zvQ|S6oz+$tMh$T1gJ)d)(@MtVs*esOTI@Q@LI^nxOJMS6MEVP)fAa0bJCR;@%1gMf_wAu~j( zJL&__jC5jC+z<@~c1^EmJW*oqCe|rXbUyh4G;Kqv3^Wv0EU7V~8BqwcB!)`z6B;oc zuq6OKo?R2eMQ6*hu;9qe8hLi`79RTsDV~-U<7A7#Cye${Dy{uVj^`y5t1jDrmyD#w zr&e+qKv8-kEd=$EM%*|GqiAqEOh32ncYz1|EJ7^l0zbUkCdN&(Y0%D_E%haK5MrUK z&O_pu@*t!c@vDTKKhVX4%<;NoA4q)6q|-+oMM!a96XMQ%_l~q;O&L2JKA&(J;CESx zw+o(F;I&gGbhrg@A*yd2n$%T)!hm+5pA4|ZC&iQ5Nb7@+O@GLfH_6R`5&a!A-}_nmL)P;O8#np7uJi$_Ic&j z_4cT5#`^$%o`~zGQtV)0GhRJtFd8;UHop$b(?3`3pKJEdb^GT7`{#!J^Jn|#L;L3= z`)Akw*|UH4?VkhtXKMdEwSVr~KcCn?pV~j4*+2K}pU>IP6NkIu07$c6Tyc192SJ*$ zRfp?#Afzck9NK^LE850bObOr`-UU7y83p>srVd1JXR9Lv?3>X%! zJHv*B51hf%y*~-{{xsD4vrzAQq28Z+y`Rt}8s(Cgj%pINZG*UsMdsv8<+mnzMnrXml&oBT6i>cIs&S%4NvkZUYj;~uX7 zs9}wJHi!U+n+_0vT_vF{z6Q0K+=I6!@+k+&$ArV7aundM;FmC*axn!4$>da0Y$3+S zl0%V2XBVJDC*!;;rbrhaROyO>$v900Fez+MTo5db)Q3cTv6^sU;Vt&Z=NHf!UP&8F z;7;izPfo?u1T>Ph)#ctWr>kG-)Pl$ajsuj%9s;&V_EzwJWlYvkyJd%`Ne?q9pSzig1YgLEO{~=w-KoAA(qsNp(LrZbUCP ztzEk`E z{tiRR@8BYTKRA7vo=v9Lq^FK1lNa6T`?N8n6r!S(v;%yYz@CZgz*|r(93xJyC$TiWuzNp$doN!f{co5)u!9gRCJ!aO;4Qta z2XCLe*!$172S=%q9lo8t29n)TNLl4~OTR|+0OW_o~ zKl^HOH0=(>KK4BYT0K4#f-fHn`TW=pzS{Bnh6UipS_`rp)_aD_fsD^qcVZ|N^Z-)= z-cZt&JJvzOtG6#+$e=^o1CRNYwhR7a6#ij+02vUtw+YBGza@xCuf>1Zy}TGk z2yRySRk+0E_u?!7TKB0#9`9aC`HKM(t6-3C^7v?FsR?tnLH*%%@Jks>b9bAw#&rgN zR`JIbIGu3e`q-y!qeKreyAl2Ca})h;&zE67PP5EaT0KW;5!BBYlROQ8l_ZNrsA&OZ zYnA~**MZ_t+71v}#7z4F1XAL;{=MgbVp!lcr#PfdrzI|Vyft_YqODtAYq18J)+30u zEFj~n)0|dC(|%gg{+rYOjnjT4V?E=45RO9_h_%qcp%BJN2n!1a9?``CEUVGf^Uwgp z#nwQA^T-N-dZ6_ZYm?|1Z`OXo+@~T7lEuZ-&Dl-WUn`+EFY&&t zF15kYB`tzPN3J*KFg3^Qy;kpPVZJZm-ao|tWl=*uu!%nd_r!1=*S586qPT9^(Wld&^gT=f zB-RB>YG|nt!es8{XtL-)or~yWsoh(qtCn0ZT1s=94JI9P2il9jE>a^ zX0x6GUjJS*)~c|!%uVNaQPh9~_v@Jf!Ke)}s2Ki1w!x+{5-@y21_0TAtstaDG=gXq zP@5^mshFstNVBnYQreL=n{p{)?I`X>DMLhZ2cvLwk@$PZhOXp_E*Wl;ifKxH0M;=@ zW@`@-Imka6?~u6xXYMD9;?S*BQS9Fy)dK)d25W(#5eWJs4vXT-dz;a&6g zZZDHHnCTG zsz4Y%=A~9LDP|PT{qoC11euhtW&Yw%zD>zAifApZSJqqrOgca1HJ(4rc zaf2MPn}8L(ORdkaMKc^$`RS78w-<@XV#**Zxt9VJ!kKkUz3puU$huu}tapKfOvczt z`DuFjd4hF+wV2AJ8cjGS^tmLOD88^De@}>BzT9<%2u#KTArdWYA>!szJff8el6i!~ zh>=V*y&Q-qy<}JNVM&pBKD7K?ipAItR5bfniw1J*h}r>e$#+wTyp~NnxpSJu2}Rrp zSw=4!i!+lebB!2U?Lf*RTK{A3Xhv$GWi+pepT<&uQfkHPmc`=w(X^^L+Vj2>pi)Gx zg0aAmTm^DLF}a4yg#_g)a0`jbRlq8Q>RF$b@QG@sQ=N^nIMNo@ z^cu0f^9ANcW4gXylxtCpGVVsLWAo72{E=}T&{^5GzR~&6`LwnQX%aJ@n(YSSNxU7O zZbsUFAKPVCSj9~e*eC{f$X>cd+WW~+1jwyL;dxE#CaNWG*L$WT}DYO*H@ zb6zy|b0s!piYs%=nB7#hhWp;{zyE&kUX$Ng^}heEzCR3o?y0YxVCz%;c_s9DtUs@R zg+5O;YN4;W`ik=2z>Ca}lQlA7z1kP|-~yL3JLO)^xq|A=Gla z1$Z|cKcNVUWp6Opx@~0Pp%8_8C<&^6<^9C_>f|RvN6*1{bd432PsegA!Epti;wzvX)Xg@@OO4RJh8O4y;cN)>0xoSyqiX!g7NQG`Hg5XIikv~b&rA`4k8 z` z>{lF8*{?I)-|m$=CmgTD%rpsrF`D2L(1b!NeiYJkTtLrBh#oiTVVIDAs?G+hKR7tN zSINI%&fY8lun^sA29yRS4!T$BfnbFt&IMLj;x}-UmquLzR^rk+JMXzR%-%k|bYmXd zV&Bre)hc&zEAO`h+g#e)KfRb{?p?CFZ$~?fh5dX{PP7+S2|UJq1;O-KgNH4NU9TqP zwTx8ii%It!9^@iqo7Urh%Pg`LW+DOrL-?0QAF}3A6QMiKVWnm{|1I-KRORurP`QEG z>G~OaNkPBF<@P*lr)|4o(>#zIpoPE{;{jKO^U?L}_yhse!HeI^pl-!To@WY&chVJe zp2^3)@wbkf#5!W>Zo&Op_&*clzy!d8XaGJrcwPyd7B>2h)A})gMV@`fJBJ5Ci&NhX zjD>ik#M-|e1h0p`fkD%or^>g5{=U=p*SphZONK?}ITc0cnpz4_nB@;O`MI>e+1Uxq zgmPKO=>fPckTMj5I@!L>Cj_3OxIX*Ofu)PE%dTD@e) zFkbC8Fwc70J+}1h4lcXnembD#VFIG8G_`t!00PVkx;B1)jUFccr_)1yli_iKK-+e4 zuqB`l4@F{q`0j_QE zo-8M&-2gdK%S!|_P}acE#q&+MwV{X2D$RxLobM0l1!uiTVVXRh*w9sf0=2tl<=a6} zKD+CHyo<6kBP>w7qM6=c7@31+URSts<1Ns;)M`(ES@t?}{%dU6R#MTTF;Qb#BtlAS zD8r?~coQF&wS5s5p&0;!_E}Cm{jLGe4AQ}r&OC_z;JR5Xi2N3z%|u8O;KTb`q(iU= zJl6iDA(qfh%U)4bFeC9kuEhFa!x)G`j_u|a&`ovmG)|;lY7ldl6|{p8mqIfLfe=f| zXtYd!-+EM12lLYEqUlmh2>LXe36-XwP`ypr*0z#FO);h%r?@w_#SRV?fRz$^xuYQP z1lXDnE0`Hn;lPnKL-S%X`2?HD90E9Sr&iS-HLs$Z5n6q);n|#|vi4|^wUFDEVH+Ad zMJ%yUe-BY$M*Y+99L~7(csGm}q#^;1%#DLfJ1>W>F&(i0ZRfaxGarMgv!koD!{(#W z^!73;Eo`+~-A~40?frI~x%8JV*sQc*+qtayP>$Ym4832|T)Y^rN92&G^4K6_lpsLiihHFk(oH5Ge_PNF11~eR!e+lL61`$hENn8m|j9Snk-h)Nwe#!^3dZj84C89mw}E z28=aNgktC$E};B=-ORuPOwZGO3rrfVbJXmqu6x)ydZ@3+tkWIFre85sGa;9j9JrE` zUs;jY8O+QrR>6z0hX1GM%hJ-8fAyhAg(EaeozwAuG_H%{t0=5X*1$VmUrCwAgSm>6 zg|nCe>_Nw#soYIc25#5@VQk9{gfp9mOFA$(xhWV zo%KQjl|7jZuCetY-QDm@Y3|_gyUU!ei;f-jWLyYD3(Y#_1l_c74mWwTf8*LzIFs4q zfnleD;^SR)yMtL+Hk5ld6k+t`a=F#)-C6<&taRp_$kO;6b83RC2sQS zCUc9w#Pj7A@o2b9ZIoZm@~e0O<0u&tU52Ibs}#tX5uNTFeHmhQ@{693Tg+E=&$0;i z#seEcYiwj}u;^cneUz3We+hDE(Sl@?Gn*_K*n8tals{2kehaA}6-HX^1%==o-=^nr zZ4KthsuWdB;bfRBj|d>v4+8`Ww635lBek0dB)gw4Qg&K`-+rUmMABpALD-a^-cg}_ z3+Y^%KWHqFa8vDubCZ#;LHe3wM}A~kdR(*)FM2V|vWp&^TdN8|fBc}1kD_kV2*hBv zl7<)23qd#_29a+;;#Pg)781ZL?>-lWFw3ZE9esxf;oe%P6c!%*L(;222p%>kUa=+6 zl?i0(jV%l;V`^yptoS|!%=93K=X7i_8&+FR%MtD5=#Ve`%=Cwqwrpt{u?m=jT8`3Q>)#0z@T9{HN3dBr)P<1KbGIS>Z?e=rJTnBHC0YF-8JZXZ0{hSw@NK5aor30Np|eaFqyWTMDb4BL=0h zmsv<5OELD@f1H37hCutssvQWslOAM=(rk2yrIQR&ib3y4N^=da5M;5NiWy!VkT;(3 z<~D%b(wDfs!zV8ib2RLy5I}di#2Ku;c}t`;SO}~rl9A0`0IVnzU(2FjQ3+G{*DM`x zhdQp@uZb9}O|akXc8Fg49@#GtBvcm9q{C{Bm>&1#e-sJ0Sf#Vb%E=EKDH9^J6-J2C zn5(Fz0)&b~l{mV;H2Rg~?EkN5y#+_EnQZd>V2pHnh3K`yxHTy|PbcTsN0Y`N1xE=c za#PpIWHu5W*inshF+~_hWqBJeA#HhS1 z3N8jqfA9;K!G@-OyG>U#MuSG|ySFVtiN&QqpCpcFo}V^^F;%xhB$CJNwidc*^BM5v zhXhtl>>u38Oyol;GfJ%1-=@PnUFbDn_hzq9V#6_ey8wSTgr>P1P9R4t{%$2YfZVwZ zY3!hJH?K11Rzg!wb=PJA%$M%#@Ac6 z(~=t@su_%Tq6TzJ;d05MOD)rGR9#&6@=b-SA=!3;jZRptmMX?JSSe*nP*idC2o=Sc zf9sq#(jJa>4Q4X1!^Ae@1QO3aGLeqdaT52SG9Yy$w8586`M25wehKXXsY*j^pO6B2 z$Hm?YN+|eHA6BM^K+Q(54=t6HN*07RZ4$N3?O3nS(A~cEO@&`rg}39Z3yCH3bb!_5 z+?Ea%gz=&%U2BePSm7?ylmO!_7?@c+Af7+VT zNRaZ8;3~S8<%IgbJBkacsG7OT9hp4#2JX(wui}qDMCa+470#&YE1J}NyxebduK+X% zWs3mSa@PS}8k%dC#-^Hf#FymO(S$PeH02I9qba@+HtC2(a2dm622Ob|JC-zs#Fidf z7^h!Q-yADWHHMfhRj)vjPyt<$e;2WcDJPJf`*oi``5-gB-Oc)PM#d$;~{DzFmL+8996Ur@Szb9kzbA`C_f70m$ zSlHfuy&pW;)KAJ_dMuuVSuF>ltVB9BigTjaLr0FjIstF5$kba+e!wU{f9uz5+DGYC z4wd)~R*DiKG1gUgN25vKN7a_@5XMa6J)G@8MJ3K{odPdjSJhI2Zc(fWCQ)bPa;BqP z2Wb`3JMlbRad8Jore*v9UM;W&?Z8h`5u*JQ|&%py_DE!(&+q$WMQ9_QVwwv*-D zFozZLZWrcfkXhM^^cL?o6cL9@BE>TaD%7bB9$k=s1Y;18p_C}5e;GFZeob>XdO<#P z1^B4VEv%LchYL1^G^QzrwwRz6nU~2g8y3RRXIkL-BZp zM;QSg%8ur_v(U$=;l2|yO#IVhv{fX^^`5@M*RSm7le`Ijj!^Ge zPN`E8_gNvDf4$ghF|W5|kylS55rDcjiwJb9s-RF+RsIfDW!9GdWYW%hxouv$fh`Z}CjNIpC<6A*jde@$SLG@ZVFx__tfE|$o{lCNJa^fLe|1zRL^wJ_zJS~e|0C01gu(JnSY@Q8m`d`V-_-cyqzeF z>cV!S&}+eNlx181y;Xl#isD;|EEMpC(S`k1BMfzKeaf`ZLFaH+CJV%-PjDiJY*sOb za7aDES2d_YP~b$RKB)j73bAa*HjT}M@fEm!S8#GP?G8u7@q0Bl0gra>H2^$gtnP>G zf9bwwPV-}T?1kr&1n_--vSfS}Fv|~+8^VU**20PJ6T;+Ks>qk5>>L%UG1iR|LaK5( zxbO!do;THB%-ZjFM}4;2HmU5*>Ag#i00eE4P^Dc$`{Oy@~|e<;l5%d}C7NLbu78m%HM>d`wpUjyUjR@R#_ zF6ty{HWo_g<{iBIY4W7r(#`%ESbx!2v~}vn}S*Rg{W7bP6{kq&S1;NLl)A^$xikNkIIL zykt_$4<~(+-ThL%{@Jb)ocL-yBl+r0qw1SrMQCLLEfYi5LPJBn@{S{x^C#ZL$mUJU z!$`eK`$Ub){p45yJi$4^%@Fmlf2{q)PF!s*k=`OGx{3Abs|5LV^K{a`$i7vFEf*8M zrBsMVc9#0HdhWgiwfgi@$8(@miqWh%#Z3qXGh{l%iIGa76k^C0sl@{ua`B2^yqZUd zX}NeVtjoAGw8|OLa`<59qp55J&B&7S=@T+@)SIE-ciPUYgev15a(*fNe@f?}rCS3t z8|uEE3d3-k57Uf$ir&2#j??Z`0cu$~I%L5GC!^RSpx2C z2eY4?m+K0 z*j+N7-S55wDqt~!s?6ldJ0sc_)!q@wL7#U^Bhb2lG>YGghUw| z@R+p@YGjDiV!`}<%tAg}o*b!-3g?SqmS+&DdZhvlghe)t-dC1MX>IQB zSXXGbP38MZ2QO9}f3pfFCqBwmV{n~Id1@L*ZP$R+x`0FRVBAu{!FT)|du8^6>^Y6x zdWYZh7?$;dC{}`J-#i*CY$two>@A42kR&m49M~hYCS+=sE5A;oZe@_9d(8n&uI)6M z*J(^^JM~C)r?&1ESQP0_&|R{Hoe&7IRVQV#1|N5%NsNtA zZGvV2U)1*G#3kP>2o2q^#o-5>D(c^|uIkIdiL-o$r-lp3OOsUIGCuEA6?mP1T?SV3 zz08hD#Y!#*f6+a6HkUQD@&$b)mmK;BSiQLDglHo=6S!FHLV6wTxrRRw+hdWS(ZAsXZ4mkI7XObk^6gX`+IHs^Q>*(9M?TN zDJx&MqKB!)5*nToL3d`ks1pG_wV4JQ0=EWmVP#9|l0$-SUvax`ZZhbWa+Q`^r918B z6TCF8f6Z^&B%foU_t@?3_!=)tkUDJ{5D-VU(uC(nr@r?Kbvs_ekeT~kpR0Yhuz^+G z3mkUZcW1)Z0$_`AJQKe4B$`21-D7dm;q&t1Joq+Rx(7b9Ao*XQo8S@mjQ#qD8zG2` zpwK?);6Y8X6NFlhNE7Wm<0Z!eXQ3UTu%PRWej#Qgv@hGIJ2 z<1#u!-SH?|$L+1b;cLu(FB_6?OhF-cS=hWsD;|{xzQ0{zN@^s}1C!I&8b*=Q703{i z$R;ux`J5@ipvJWnt_<{VN-fEDJfRJbuj%OC@RfB}(e=)^M|#VG7wNq3Q)f%#RPYY= zf3Mn*k}MJxeSQjWW}Lz*OZ6~i#i<|pgp#YvLmoy?Qm;n2x>_m*90}tm?N^ZSTHaR0 z?^E+VhMiUjdUDN?jAS&GSWsQcUbL zy}V|W-+)glda_TzmA~mhyo2Zbjk`B#xBo$qbnx7&q|8aQB~$#B4q8didLJ)de=7(} znWn1ZyXpVot!6=d!ld|X=X2WQhtHN13a6dYnWll99*8t|4TgbI(%CKmS zwzJTN%n(Y)NeN+EEICZG*?!qQS9=LZFbgkMV~$AnM$*SD$_kcfkEhymh`;o1Dae$2 zQ=a;fuW`Z{$^{lWTN2i{=aJA0e=^UUF=+J2u;!jiAqIvIf`%AD9iZc7K68}<(0rAm zJ&arOmdYlhpO%BoCL)LA`P8r`bejFLW8$mPH@e@o4&lm2Z) zAd(NJC36Gu`P-L?xa2v%`~u0<@uAeO1@ErP=|Aaxgz3A4)1MOcW^I|U7m#DyOAJDy z-P9%Ys}cg3^u8(vL8T11B+z;?#xL749+*867QP*yPDTU#Bs;paeWaX-Lh#gF?z7^s zYawgYiAkrV4vJ_Dj?2fOe>$kA~bOgLUj z_Ai#lg^wjmCTBTgGNrF3x54;51wI;LSz0=or1aR@jw) zS7zpZ0+%95aRz#)HC(6rpR*eVcy_p4B;stLu6WKu)2L|JoObT9e^)ruq&-$)QP0aI zy`SYq(w{=Utgcw!+v+bw^61Umy`aovqIUsd7Kw-cPeJoIuR%j+TZMC?ey=mm2)Co} zIUjW2i=7Qq`p(2@kRXieET)xZOnU823=t0{f=u4DYN{t~>( z)6e2D0RdR^Q&cn`e`9SbC^iRHSgoBdMy);HeQ|jEdQClKkG=h^*#0LgHWY!sHQV2s zEvnhZi_vVa-oAJdRBZ4-&!QCDs#I*yS+QQL-|LK`>vr@#^_uScf1X|g30S;ZTLeRE z%En(yt<|HbXg>AwGSB7 zy1U?zggK5_e-@a|-98i1v__6anC0O8UC_)E9ez@6)1K(Q`7 zC}>q1J5yGgJZsYAQP3)-($4hRdU-nS?;;H~-vzOyK~AKIEYQ~{lfgAR#aH7_zu5Vw z46vv=CcA^n?zm4OYv#!;#eM#6(~I;9-h{RM_JCB2e<6r<4&g2O(xUyRW^E7R%krc>S#8%BkQ2PabB8g}21lO*sP+*^FQ z>v{8^e;1Ry+JgX}q2~8^a*q@kT+432aMgbbpdidgpQM%3n_<<(9GlB?7LR6O297@K zuog8I(&X$<#yJGOnv*~^2lNABs)~8-N*3scu2juwu$zEc{V&NP#7l#peh$1Mwy>zn z#aIw8p6XhtSmLoBYAJE5hfKBl?@RmC}MNoKOX0L2bFk3T_}PZjuC> z;N{eP-xdwBXc&3TNe1?dP5RP`<&V1+c6wu5@*WQS(;dAWjxWlD^$hCFE35mb4ZM~| zfBwm3lZ2y++$wAjhwp>0_%LKMQRTL9h1^S2cE29}N7Lci87j=$0(Dz+E=cN%Pga!~ z$>vMOy#lk$y}GZHeuEI?DqMZpz3!!tKZ-q6oq%4OsiLvIT8i*sOD2s1fkya=OY^#A zkmqSYy!HymAq@@!Tl{5?Mz+K|W1((ef2wRb=~5Fq*T46cjHv+=N>kuWL{m$;zsM!$ zX(G!s(Yf{i1tTZ8Lp^|VE?||o^6`Ay?bjIYQ&D~P@rKsUfJ2cSaX=+J|3 zj1d)oVa6`Y9_7}x1(cA6B_M?@0bAY;K&mBEJiFPIwSXb$>iVe4dtBT*9a%B>u0p!1 zi48f9AN+%e<%k!(4{#NJ2g5s^lJH=K!L+4Ur7vH^j<_UBI*}(9B6_;WFkL+YL~OUe zBMpp~C1}+_Oi54Zr3MMbtzyH{fAo-06~M78Xeb3Nkit~})2ZPAE#(`BSpE)`#k-cr zgO)?#JkSFo(<)|H%jLy_yDyX2RuSV{4&Mv1y;M7DvJS7x9;MRfah0~1TvN~Gnu)0} zWHPs4)W*kh#0pGciDc%wnupTTLFFxK;Mz!%r>=SnRSYQ^g-Ii2f~~9Wf3gVZB4iX_ zk|G?gAK=BG>r4lawB#+@X?i*wi*YM?of#kHJq|s}OV{7w^NIOv`!{(8>d;HgeAroR zMe&s@l}2+R4?3&fF%iJ&*xiQ*Jy+$!X}yUo#tLx?jfFo9Y6Ob1=IYzEM-zRkV>9{K z#hVq*v_!U=1QB>gqcAJBf4L{(&C2P14w+21lg2=FHxxhEDefS7oQPK1z=67rfon|E zM#rg(D1=Q6`hAmIAE|OGkOwkDOLz$W~#C5Ze64 zkA*|6t-QKpG|OBgiTqAEMcCz{phdiFrAg7bck4d!=ubYhf};@~f58j~+guYndVxX_ zW>C^!idk&pNtQZ&YIxFWi$yU<0isI zjZ5`a-s-gXu&P^M;y+bBpyJa6dJQ%FG~;_Lmq9GBm+&3a@{OqXpiJRLR53_UkV|&M zAD3vlUsl_DY8Yzwe|b5>-cug4eTuv|s}R$y)W$ycd|B3U^{zh^@7+FyHg08@su3-K z>sE1sTLT2v+bJ<31Fs8vNVhzMX78`kc(z<>TNbhN?7c#Zw!Qb7-8|N^Uu+?VSMpo2 zn_-%ND!DEDsWkbPu2|)|WIVwZ3^N<#KyEE{wl69Ma%V}!f6CGgmZ;z=FJf$YbFK<2 zYy9a+b`)_Yu5I!Fi^=1ZViu@e_!a<{$(slzIxvv2yB4MB=`J z#RH$k6%p&&^kG>-rS6D2@VpBsg|3MxlcKH(i&ai7f1VI#cJD+%u%XURGn40nX3F<; zT^z8v`5k;0l07pyFSv^WwU(%^r%nPO-w1) zlwq@3(wIUvt;0a}Ec7Qm2IE)-2`H9}CN|GcVax#%Pn;F4t?M1P+b3@BEoe(40^{*z zI+StNf0#?_qq3V+GA{bweml;(U=9jq|I$hhF7ks@F%c$HmHGw)r}2nGHc;*)`P~VF z0dXXb+wM^}v_Lp4Jep`Gwvs`biLC@<6yxg%pBfABm0nttEEOX;JcWxa0Lo(92;L3j zY=Z)1n|k`-@iw-S7lDc!Lq)-E4I{|+vi7>Q9Jk46(0}kg_<&?kA^{RA=0kV|LCsxQ-6wm`!rRuJq= zepm8ID5~y&vGf?|8->cBP7i`XxKLtRT&x%*( zcCl>&8U7S*bzpQg*vobZFyE>DVBR$Q>b7n+`cy2x~l;c8P^-_}HJpuai7RGoxkv16Y7$UBf&H-k!lKt(quOZ9sdOxS zW)z6VB5?>tT9kF5_V)S$4auMdI0nqdMT3GXH+t?>AGJChbFo!?vb(Ox9S@jXwq{%K zefTy~3i_f6rgfvS2uc<*lYf5LvKI)pa816y_2XY!KOUd_X_eve$*h_$*7Exx zUeZH+r2aa(bZ)JUWj*ON?2gB1;wcK@b5?IE~Pn zA0V(+q465D{;o6|3~#qv*9W*-fg7ug8@D8CRmfj31`B6pXTcB`O|OS;`N(&eo~x*x z<{rsE{n7Fd3eNcP(GfEREPwdY^~w!U@+`4MNYG!#*B3dBsgCvcKfSs&j?T=AVkukw z4pQcwo>e?#oB!yrT1Q*j0IF1xm}9~zOAKpsj~x@+!DS+r2?ZZ*xrJy;_v(CGC5Q=! zS?aqLrX=S-?8_8%=5G_WH_ocjW>MoYM~mY8R5DbnT;DCcyld{&#(ysDnw`tM7j}zo z)Q0e=aFce{TePM-|JrHQo3n8k-~9bc8PQt>^+E{xw_>B);(%Z*dS1HMyv+s}30QMB z!187dpCF=Md*rBVe;$Tv8IZ)LOx~ zC>f#OeQ659SrZVduH5{6<+`eG)h#IH~5QIP)@2!qn{A<3i?UZ ztDv7kwG2pLP^NDDlxZgbwP@`m(JRzWP={$J9MmFs3)4+OQGcs9{n&-8uv!WUWYGm8 zwxZnH+F8CdgqGA*EwU0vXh1640QsU(^53o#oV_?pg=yct8cxo>@rTN+)pY;teB|8= z3^GfL_iat$GBFKJZNn!-54nUN41l?~giw)3?u|R-5has!U{KG5ntAU6Q(#==FS@WF8j1e`>lHoiwjpyl>73{ekL_}u1%-7kfx>wefIZpr z%}Fz{GzMyvy~2t-lr5&5X)c{l)4@={NOhVksISZ=^8GwM+JRgLGRFa!dvanOi7Azd z>YK??vb;mN6I+nGW+Y~otbWu|^D9{vb?9$*CKA+5s2rV;P$Lj--o!j%w&LCQ) z5`Ps0JrfbJ2HKNhS=W9=)%T(anWb+-T)C|u?)}yYgza4&LiqGS9Z((Sj0jt(kgjw$ zKDM7lIWml|h1sp>;a-6EKoTab9ikLH2co-0*q_C2o4L)Iasn)`M1jx!#4*}M?CI7%aa}}2$Fn^zK0AX;?fO6TzZ{<7A%(yexq(F^(Dq(yo zd0l;H*c}t6V1j_nNr3W9iBAfi<53UxZ9HKsC(a@#=5;azcq>UhG5$bhsEkFg!|u2O zo%cG>L~!^u*yMX@wfuxU1^e8?8-I0e zSCtz_S%kdMzA`M48q!kYgMt=dhSRUogk|zVN--iW5tt>CqN~|*Vp`jo(sz3kp#+9m zt`?4=_&;bGunlY#OAzA{<*Wt<3oRFPNUbpdKhYI)4GlMwaaX92kNB_a{S!;&M_5U3 zt|SAMAY4JG9}VSKMD`sP+!H>Bl7CNAIR^(i5U199e>US8fW*XGwQ+*E7adpz)w6cq z{uDhKbRrnRGVw@;I^c7`eW+jgiS#S(fWAnWF}S&SIz=ZE-Xw@)X6E%Ypa?tj4IT>wd= z2(UnH`S!Cn!}lNZ{Xsg;hxv8G@09I^>l-;1q!z#b7fZwB44T74zOf7N!1qMeljrK( zt}LpR_)^eMwexjU)}+;}#q~@^>C{$fvusWfiSRZgq|h`2qT1~H&9#O-{cm;b=NfqR z^o?kjY$wpCu$R)q>v7(_YJWqiQ^{-#!qv@p)-e2>a{PrI=gHpmGxjwar6`gb!%YYfSC|?VI#;lwOHR_xPxBcPy6loyJr) z5W4QDl^iwk=y5U`d8evZ?D$kQYFxFFtLSm?{&c#a{_a-m@bLOfY_6um{w&?KlIsYC z*G*wr!(%L}?79evU4LOC+#VwG)IM>Lf%MnfNVo#+eI3OwyEWuE5_iMglA9cjgIEgc z^UJKb29R!mXxO7*zVU63k4kNUt$+xF8Aih$AF=+7#hQ=~<{zG`llI6YP&>l!<@D@qe7;-O<5xkivee4ytc_ zfl+8h#9Dnetnt5jBWQ_ZY|w}Od}ca=qQ3x2YEbZcnl5+*LWo6s?+T-F;WALfnz-5v zBDg0uGnd^F>~WRhuplIB4sFzg$X8r_jgvVgJVz2l? z%-v!C8}2CN1G4rG@Zj`SH*bu|6)kYbM^EU@6WcDj5rsEkkG`0^Z#+x;z#E~zFU4+D zz-jloS=vg*;7aIN?IfjrL1rHZBcB3w__q(H|DnqwzWwhKU4I95a4I(LKnLx?;&k{h z_cOZEEPwbzFLo_0FEtBsz^-&X8N0l`r#A_mb#*GI#=)fK6xo~v;Q26p%a!$8;s1A)Shy|;YNE}wr$G!BtL*~|Lf z^YlM2Cg7Q}QKdgLY+$nJ6&r~1Hnk+sUzdKrw|^vh_V8~pQopr^OvG~U<2IWElf zdnekbf*}bC_H%GbFW7C;O777yJhdGn_wwmQN_=OIhkJN2Wqa__{1wHb#*2TiCqc zVSk>F(!KFu*d2>WprQgNW3d{by4s`xOh2;^F#Eu#dxJG@oF+#ToY0$MjX8e|ja$h8 z3U=;DGY9swP@W0YvS9`fJT=@mfL-;0J!#d-x`EXXKOVC}F@kuC*rzV_$UoUV+-o#Z zUEv4i_yvOSPx){!U&@(wB3{@BxGp{%41be2{FXJ45pu;Orf7A3$kchY1x76=!G-LG zy1KED74wFQ{fHqU_A0EIO(E@br)I}17%WLYwwxgJfxvNKJ|B1BO<95KfH!eCft4^l z9*v>y=Hw*8$iRXg=A5;pdkc774l@pp0qBa&yJ>ov3OfzDVrOiUsFjl-XYr%~9)Ft_ zB)v$-tMHbm;g9?v3Y#&>v{n(t2DG&=vXH3C73%oJ@)AH}7*_}zftKLmkVUp+Gp9om z;+h_CT`5Tdi@QIh#H+2X^v;|(J-z`Wr)M)(loNVS&7VS2&= zGt6*03>r@5rc;2IOe&#LU{bF{C4cYb#po4yDBk1o*6u|o1w34hM1nWSShcOgm`ZcPc(IFt>Lj@TB%A);eQ~*ps;`p zdt7ZuTUJdap!?$#wuZy}TFPgH%!V^$hzR{hW2g{}xq~~DAKUL@~ zBrq--aF~3NcWYzOw7YgQ#oGFc?QlXX2q7#r!R6YFTj>ZojiS1{j&q!jLa48hYF6H!;wNG8HcPfeY*T~oll z9kQw>M*o39Y1Y6Mu7CWo(6<8BqpJqkAUW(}=f=V>e6;)I>9f7(_gE{r<=a0sRU6r1U3rbV`3hPrC-f69eI?f$+>g*fS8G zO9&_Sfc2Wik|$oPo)?jG&Ed%6EgXnj%d^+Xtc$ngiO zk2a#!cmK<+zOmMMq^rL;_^lZD#@gyithNvP=e6}UU3>TNaR1j=d(YmzezE&%?~vB7 z-sM9S(yuFceNPCJkRq7Qpb0t~JpPw^cJ{}+8DuO@2Y;_e-ErC&vYzcEe&_HVllTpj z9bqwSpph)Pr6q$t3!!naQv*)}sEOK!>l?kx)pcxaj_yE5b=JlIben$;-+wr~m`*3} z1;!k}IYU)K@y8S(p2L6q@xwOC0QOsI1YS(ORPEmzb=|!;!dCBIJKg!A*vWUN82lUV zvLV2S=zkWQl5=6$`DBB0javEG%0?ctO^uI|mJ&wzf_2`sDEPUm%($NS$6H=mGet6N#?(A$SNsPyxWdmw#7 zZf0Nrg9TZ!(_gHrjr2;aBN=DPw&F@XrpN$NI7|a(^KQW;w!8JdCcG``Cj3Zitf{+q zh0+DiM!@!lYTYQLMO)cUkdHUfWQCL1_$vT22mv2*l^YOI#A#@e%;b=EoJ!f#@VVrUt7t|SqJ~SdUJ;z3`40<7f`IXWi_b>a)4-cZ^Pc>sk^sG!kK=y z#uOvM_JvKj{UYi^Id=o912otc+YJH`@qdyiKCwdg}BH_RD4~erDS|bgvidm|I3n#o*=1x;5Ec1 zbQTq+5)gvc0mSAiW2*H>V7=7s7h=L$sF$L4W){EWvlFxYEn*>OSGVy%dVkv-NXyk$ z3C=9b_HjXmuQM%JXSPRshOYc<{fv$Z{N3Ut3m%uCu45(#6*%MbBU2ygMAp5B!L&KEVK} z$swPL)<+UL$KI+~TO5IqmWJ&r4K`Yoh@b@NnC!Nae156U;9S@7Im2Rm2plO`?pXo| ztbbHoKX>aNVguRLeF=l==rj#-Fo;QH101$wRX&w!iGb`qVBBywi+@J^Qce-(ec6#g zGf~#NTUj9JW%s<{`EgpwWi~S*dQ0ofy5R01<2F8B1_Jyp#;4RU9n{<>=$u(MmttNI zCSS(+B(ODL9mwpZaZVf$VPoWh$W%i`BZFz5-~&bD^eQi23;^kXM-6T#=^4+_2BHBf z7znINJn~Z$|N3ZsZ-qJ6WvGQIv4G#qLb6=^e2z@va{q}`Az;l3|-(on!G)F{*Y-q z@3x^}?Zt4MKY!fWv2zw3KHcA^)>bo9UkZwSX<*3jE6X!f{0*zW3_liMI;#)0I#OcW zH^8t(->MD|DPjqB-lC17t?A*$52v=5adiC)mL8uv8xGi)!8Uw zmLZvQOJE#iSG@@xzwODBsfDAOY?=OTn17HZ7%ZjlVSmPFfR3FF+$91S`J#d?b~vmBKY1Z4kbMvvn{AI=F!+#T zf2;av%X(bSMby;SsO#mhfIQxH6>?;qod{h)c$#yL-^CxP{fsX0Ty7Hl=*hl4c>5H0 zmR(Bfwtw_@HBS4;P>hiSDj-5_oqv(6vp1muz&3dfR4Uk^__uIXh`O_?LSUW0qXsVQ z7D=+tAB}l@7AUiZ$v^;#j|u7&A6{^jHdVYMAyY8K5*y81_=m?{&bHQZA#oZSM=&2^ zwJKW{V~qc1`$>)8=BE!W08qe#z}i8pjP+`P!+#u_9FP75>ii3~Ksuc&R|Z&g62SZ` zXax@S^;;o#;EQOK^V&(%D7Sk4Wtj>*P+fYJ_T9$$* zXRPV%2%6}?k+janEs7f07jD0Ggsp}JQdis@x+}<=)8a=8oV1wKu1NlL=Y;*qMn7g+ zxqtPvIra8?1gDzw3OcT^?r2%3Xaa>%+#e$Ef=MW=911?uf@%91xM!1#UJ#tx7t1A> zLS`2hC##@)DQ7We&6^Ze7*HJgt2YLUzt*%l9Zs|Sx5*T}uI3a7tsnF4F{l%XN@H`k3X=r)JAWt5Dzw9=Oic9gz)AUc+6IYC%fuSXVeH=Ll!uoE!myH#GU`0#twjt5F6-MBQP))hb@# zx=j9&bXHc^^9bIE%{Xu6HuX?S>iW|%p)YVp3);b%V4eL(W15@z}R=l8e z75I_4QLF)xyZ)r{g^x_~_;Dh@-fRG7-hlZl5-l<}Kxx77wpc5FsBil^1q(#+4ZG@{ zvnhGz&39>|DY@CI0hbB(nXegU!*8}*C&tDJ&HownNU_eOi!4!vab_7pxU8D*G?6we zA5~FrSI~kJ%wiSYZ{8UAFYT?$hxTS0<;9ah*cpGXu2g=eBcTLC^}cx39&N0E0^A5x zCQbPT-%RtrUP|>Sv|I<(TtgrMKUSJri!l~i^7VBy11tI6hjf~LL&L9F{CxgOJd}W0 zhib_-N_2d0{P0h@H4biSqkH7`_6>0DO<;K$Sf?z#R@T))nASZ{~@XqDz@X0mHiutCNmCmDej{&QzYl=H?u&mu2 znn8~`g$#;KntBXco6ig6@v(RZJue?Ip!&mb%08{iPmP9w2Lr#l4!CtTR)U}-%WC1i&@1B!T>V*YOn-Jfb4pWQ#e8W{p|Yzq z!k17s2h9el*R*`toCq0(m9|e2PUy`(b97!CK0SK4&NulFBHZdcS`}M@>mqNZt}4j8 zDQ0hrHL1XAF5>lAE!b;#9dN;i49tH@yS|y2y}q)x%9+h7{b4|eB^v!Moz;kMSuq;y z#~abI@|Z-1&oVA*j$X^Ot}u{}_Nh0P6%G_a)?n4`@Es?@QcllDKX)EMbBgX-1BE-&S@H@9{O3zkilakvwK`FF-ijCu1+_LqTeRy(hPCBr{Ka#c3DaI8$ zVv+T{gOkR!Im)enz}0!MQu}|1i%+-343KU8lvqr~+mD3}k+pW5S^kbcywU4C2#nr! zh0!ykZ2AjSD><2J{DEg%t9Z~gk36i`mj*{kE=C}1`)P(VPj{2~J;cJcAxqA;e`NZw!ini& z|3i9~+UKH&>2%l~4gWx&Tl5Nmaq&U`cu!Ez{A+$}caJQ#qm> z^~$a;gfd@gqB%Yl`seSEnud&pO)GT(>()~x_tsX@jeFk+9|r9(%pa?BQ^(>bb>7o_ z!fVf8rJWaTLz20@t?Pe<2eT&AV_+*ZH+}Ysp#&=Q=(kQEQF`H#-*miF`2uAq${(j> z4;}0rY8&t7IFnN$Vo$|aX*zhkx6=T9HKZ56=?UU=I-N{6lRcOvDyQMWMc$vBrEl=3 zXl3nhGz7k3crBFEl574y?+!;x4eUTqltDM|A~n*@e*b7k&;)-DU7?Za$~owwO?W1m zy5y6e9Hm$~NSe~wPz2E}N3IAn zp*0>qf4U>4&lfTGw0H^0UfxNbKNUDWe`?`I6~QXV6hwD=NY>wf(@O5|!4%P)r0MYn zR&a}Jz>UgNMwZr^HI1p3h_@gS-djQzP^Tv(wq3wPHlKgqc=L&9pK(gP(I87?LvlE? z2H&cp8D3*%ku)&1^QMxZ29cpdv1U0+B*ew@s8M_J1aWfbPZ%MZL)GSw6tXuUWHqLc z2ULmgtMtnrK>rP)?*T|CYVw}2&g|o&ORI4LN(mqFF{T34*wFk3Hp?kL<9x3+*#lDH zOmTY}Y6gGBBwxroYL1!{0O@r_f9mnKj@+x!*7$Hin*}8~>ZMp2L8!KVX!b8c`j4b= zYw&skv=YngFspsl$q-|R1Y4CYlA6?htT}_XJNvc;Tg!ZXtd=N6M9g@#beQ#$pTF`) zCaGGk^;BJwb9HIP$+}c)Y39qaJ7r5ufWX2`?@$r_KTt~n0u%!j0000808MWblLX&5 d4oz Base.LOW_SURROGATE_MAX); assert asBits <= 0x10_FFFF; } diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy index 98f73258179..5ecf0d5b65c 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy @@ -231,7 +231,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { } function - {:resource_limit 4000000} + {:isolate_assertions} DecodeMinimalWellFormedCodeUnitSubsequenceQuadrupleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 4 ensures 0x10000 <= v <= 0x10FFFF @@ -247,6 +247,11 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { var y := (thirdByte & 0x3F) as bv24; var x := (fourthByte & 0x3F) as bv24; assert {:split_here} true; - (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as ScalarValue + var r := (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as ScalarValue; + assert EncodeScalarValueQuadrupleByte(r)[0] == m[0]; + assert EncodeScalarValueQuadrupleByte(r)[1] == m[1]; + assert EncodeScalarValueQuadrupleByte(r)[2] == m[2]; + assert EncodeScalarValueQuadrupleByte(r)[3] == m[3]; + r } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect index ef71487de53..b94f4205220 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 74 verified, 0 errors +Dafny program verifier finished with 72 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect index f4d87ad8ec4..842d05da0e6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 43 verified, 0 errors +Dafny program verifier finished with 20 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect index bb162a4e111..08e4e6c0579 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect @@ -1,3 +1,3 @@ revealConstants.dfy(10,19): Error: assertion might not hold -Dafny program verifier finished with 5 verified, 1 error +Dafny program verifier finished with 3 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect index fe0885c997b..f313d320b79 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect @@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold revealFunctions.dfy(22,12): Error: assertion might not hold revealFunctions.dfy(49,21): Error: assertion might not hold -Dafny program verifier finished with 26 verified, 3 errors +Dafny program verifier finished with 14 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect index a023fcb4606..a8368f07c62 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect @@ -9,4 +9,4 @@ revealInBlock.dfy(81,10): Error: assertion might not hold revealInBlock.dfy(91,14): Error: assertion might not hold revealInBlock.dfy(94,10): Error: assertion might not hold -Dafny program verifier finished with 26 verified, 10 errors +Dafny program verifier finished with 19 verified, 10 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect index 0c1adb59b33..1e2e3944d0c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect @@ -21,12 +21,10 @@ measure-complexity.dfy(19,4): measure-complexity.dfy(19,4): measure-complexity.dfy(9,13): measure-complexity.dfy(17,4): -measure-complexity.dfy(6,13): measure-complexity.dfy(8,15): -measure-complexity.dfy(17,4): +measure-complexity.dfy(6,13): measure-complexity.dfy(8,13): +measure-complexity.dfy(17,4): measure-complexity.dfy(19,15): measure-complexity.dfy(6,15): measure-complexity.dfy(19,15): -measure-complexity.dfy(12,9): -measure-complexity.dfy(5,7): diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect index 4fd36a1d403..a18f6ffc547 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 597 verified, 0 errors +Dafny program verifier finished with 590 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect index f3e2b391bdf..1a4b8ec4f05 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 491 verified, 0 errors +Dafny program verifier finished with 486 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect index c2bb304608c..79537616855 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 444 verified, 0 errors +Dafny program verifier finished with 434 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect index 0d2842886fd..0106799b5a5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect @@ -22,4 +22,4 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop -Dafny program verifier finished with 112 verified, 23 errors +Dafny program verifier finished with 108 verified, 23 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect index 65c547aff38..e617b14d52a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect @@ -23,4 +23,4 @@ Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreas Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop -Dafny program verifier finished with 111 verified, 24 errors +Dafny program verifier finished with 107 verified, 24 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect index 638376bfd6c..45df7d21223 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect @@ -7,4 +7,4 @@ MoreInduction.dfy(87,10): Related location: this is the postcondition that could MoreInduction.dfy(93,0): Error: a postcondition could not be proved on this return path MoreInduction.dfy(92,21): Related location: this is the postcondition that could not be proved -Dafny program verifier finished with 28 verified, 4 errors +Dafny program verifier finished with 26 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect index 023b0990012..b49c1470365 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 33 verified, 0 errors +Dafny program verifier finished with 32 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect index 35e54b59f6f..e7cc92d0e90 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect @@ -1,3 +1,3 @@ SoftwareFoundations-Basics.dfy(41,11): Error: assertion might not hold -Dafny program verifier finished with 53 verified, 1 error +Dafny program verifier finished with 52 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index 1ba70097ea1..e7965e56414 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -7,4 +7,4 @@ git-issue-3855.dfy(434,36): Related location: this is the precondition that coul git-issue-3855.dfy(1335,20): Error: a precondition for this call could not be proved git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved -Dafny program verifier finished with 101 verified, 3 errors, 1 time out +Dafny program verifier finished with 99 verified, 3 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect index a7d4037754a..a360a1d34af 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect @@ -2,4 +2,4 @@ ArrowTypeOptimizations.dfy(10,2): Error: function precondition could not be prov ArrowTypeOptimizations.dfy(10,2): Error: insufficient reads clause to invoke function ArrowTypeOptimizations.dfy(16,2): Error: function precondition could not be proved -Dafny program verifier finished with 17 verified, 3 errors +Dafny program verifier finished with 10 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect index caca1722291..36b67dbf599 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 47 verified, 0 errors +Dafny program verifier finished with 46 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy index 30b324a028a..9aada7e7404 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy @@ -2,8 +2,8 @@ // Also test old CLI // RUN: %exits-with 4 %baredafny /compile:0 /verificationLogger:json /vcsSplitOnEveryAssert "%s" >> "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" -// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid -// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid +// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:2,.outcome.:.Invalid +// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:2,.outcome.:.Invalid method M(x: int, y: int) requires y > 0 requires x > 0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check index 90c7b48aea4..f44eb680a92 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check @@ -1,25 +1,23 @@ CHECK: Verified 0/2 symbols. Waiting for f to verify. -CHECK: Verification part 1/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 2/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 3/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 4/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 5/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 6/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 7/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 8/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 9/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 10/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 11/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #0, 1/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #1, 2/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #2, 3/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #3, 4/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #4, 5/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #5, 6/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #6, 7/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #7, 8/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #8, 9/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #9, 10/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\) CHECK: Verified 1/2 symbols. Waiting for L to verify. -CHECK: Verification part 1/9 of L, on line 7, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 2/9 of L, on line 9, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 3/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 4/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 5/9 of L, on line 10, ran out of resources \(time: .*, resource count: .*\) -CHECK: Verification part 6/9 of L, on line 11, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 7/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 8/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\) -CHECK: Verification part 9/9 of L, on line 12, ran out of resources +CHECK: Verified part #0, 1/8 of L, on line 9, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #1, 2/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #2, 3/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #3, 4/8 of L, on line 10, ran out of resources \(time: .*, resource count: .*\) +CHECK: Verified part #4, 5/8 of L, on line 11, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #5, 6/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #6, 7/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\) +CHECK: Verified part #7, 8/8 of L, on line 12, ran out of resources outOfResourceAndIsolateAssertions.dfy\(10,18\): Error: Verification out of resource \(L\) outOfResourceAndIsolateAssertions.dfy\(12,18\): Error: Verification out of resource \(L\) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check index 5d27b222f10..d0b202595a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check @@ -1,12 +1,7 @@ -// CHECK:Verification part 1/3 of Foo, on line 6, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/3 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 3/3 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 1/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 1/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 1/3 of Burp, on line 16, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/3 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 3/3 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 1/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/2 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #1, 2/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/1 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/1 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/2 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #1, 2/2 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/1 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy index 9f99b707598..9fdfcd621bd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy @@ -1,11 +1,9 @@ // RUN: %verify --progress --cores=1 %s &> %t // RUN: %OutputCheck --file-to-check "%t" "%s" -// CHECK:Verification part 1/3 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 2/3 of Foo, on line 11, verified successfully \(time: .*, resource count: .*\) -// CHECK:Verification part 3/3 of Foo, on line 12, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #0, 1/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\) +// CHECK:Verified part #1, 2/2 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\) // CHECK:Verified 1/2 symbols. Waiting for Bar to verify. -// CHECK:Verification part 1/1 of Bar, on line 15, verified successfully \(time: .*, resource count: .*\) - +// CHECK:Verified part #0, 1/1 of Bar, on line 13, verified successfully \(time: .*, resource count: .*\) method {:isolate_assertions} Foo() { assert true; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect index 5436a7e7dc4..e352fc10535 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 164 verified, 0 errors +Dafny program verifier finished with 142 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect index 42324885fd1..3b71b05bfb8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 56 verified, 0 errors +Dafny program verifier finished with 55 verified, 0 errors diff --git a/customBoogie.patch b/customBoogie.patch index 3f1b02ac97e..c9ea056313d 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 149404f58f0..7c3402da97a 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -448,6 +448,10 @@ Usage: dafny [ option ... ] [ filename ... ] /loopUnroll: unroll loops, following up to n back edges (and then some) + default is -1, which means loops are not unrolled + /extractLoops + extract reducible loops into recursive procedures and + inline irreducible loops using the bound supplied by /loopUnroll: /soundLoopUnrolling sound loop unrolling /doModSetAnalysis diff --git a/docs/DafnyRef/Statements.8b.expect b/docs/DafnyRef/Statements.8b.expect index 7de2eebae50..7e599dfb192 100644 --- a/docs/DafnyRef/Statements.8b.expect +++ b/docs/DafnyRef/Statements.8b.expect @@ -1,4 +1,4 @@ text.dfy(6,12): Error: function precondition could not be proved text.dfy(3,30): Related location: this proposition could not be proved -Dafny program verifier finished with 9 verified, 1 error +Dafny program verifier finished with 8 verified, 1 error