From c7f54cded0b80ee85592c267555e07b6c2b83d74 Mon Sep 17 00:00:00 2001 From: Guillaume Petiot <guillaume.petiot@cea.fr> Date: Tue, 26 Feb 2013 09:37:13 +0000 Subject: [PATCH] [e-acsl] article in progress --- .../e-acsl/doc/memory_model/article.pdf | Bin 111682 -> 112317 bytes .../e-acsl/doc/memory_model/article.tex | 2 ++ .../experiments/matmult/matmult.c | 21 +++++++------ .../experiments/matmult/test_parameters.pl | 28 +++++++++++++----- 4 files changed, 32 insertions(+), 19 deletions(-) diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf index b00f251e110513423e61ce008e590bc54554c3cb..77e7a22ac1a26716f6bd1b29bd34381c0e0decca 100644 GIT binary patch delta 18137 zcma*Nby!qw*FG%WE#2KPFabk%NOyOa0wSd_bb}xz-CfdM5)#r4(jna<A@Fg(`8@JF zj_=+4!R$3_U)NgaI@h`O%<Qkb$n8hSUsm8?*EeTVZC%0k{;AZz{@50NGmrfuFL}Pk zNs9P8CotSLPD(D)OEPPUZz2eBX?U(2VH@o0ug=S3!CQ=VtXFhIC`uoj{X(dU>(8gH z#<@kT>`Cj7RHY<@y{D_Kw#el4Uq&!RTEE<fukX;QTl8x)e#yHKzZ`vSGF6N8M!kGx z6?Qy+Ji+?$Jll4b#qD%#mxslQVo7}o4lmNc<^z$2$nar2c-N<HZcB}&J44Z06VpFi zhDGM13;l`dM9S(h%_kj3WOY4umNq(~*Qz}7L^JwHaQDEsVmR!V8c`Rm@AiWzC1qyH z*x%GD6ZCe)^1-?4rq<OdUjg=BGpy&G?ZS>X&DB|1@q4;<{+!tS9Ah)u8N++IIp?Tp z*UsU8j?1{jXZ}ll`RlZCsDy;9O@3nUY%i02VyrNY*UgnQkuh^LlumRXFRomew%|I7 zFc;iaEKIGA$J{y6>b%0#e6RK%u_yREMBa;CWnmDrkS|JZ7D15I9#Ik?KuSwXNDZ43 zlxoR6t-EJO!^6kxTsGslS~<YK40J&{mGM8%C-_deI}veCcjvC?ceAT>^AVk7zta7p zHeX{B5xLa#EnBx+M945eRV3JS2peEiMq84vpvya(qDK0-#&P7vv4X>-H)PdIn3s$o zitj=4RUz|hP(ai;^>|I7ghv~$LM055^oC=w(;C5kG2XLW2jHS(xWNB~Hs(;0V#;RS zD_)0rBv%YwSBK>5%hchrwbH&&17$s?>)dfg71vH?y4TKZ^{vd1us!>4jndjEGY+if zA3A8R!j3`qxD!kFr(VY9vX2m5>1*!`9BH<)NM731RMXjPmy&TwOdDa#<_Q?A({#1_ z69NmuWCZ_??f0UfacVug*;Y&y0w;J^(AUr1QF)xEoCC)+qOHVZC#ag(7^obGIE?{A z!*pT1GmZ46(W8uC2dqE7%X?cm%}*WF-rjxtH8@zf+FdGmHk<#7LaJkIz9u|TwpS@I zhxn#`?ttU|PBLu3ELhjYi~bAjJl4)(Q!wC9&0Fk9%yL)8lg;%O)L^wvYvV!TGcVQ^ z(Xn2q0}&3?{FN2iInYPcf|3#4vo`@l5inqCO=5ZfZU&<`2_hRJNjDK*)nV9Lxrw4U zel2OB6|KeiVt{yfePj&jzL*WmISMkIustSgh8)X`H`zN=vmZPtwyfc>53txpx+6(4 zik&<PCe?&Nkv56f8`rVh(IhpMeeauP%(us1^pddIICS1}+wfbVjh?q_+6Vqjc`!nW zLP*ofBdnf%O^2*Snfa$^$7N3KQYGMUeLg>2zT~As8@ajSWUTrzJF=FP<D>3u$Rgg( zt`UA?e7K+*x!DNnL{&;73`@MZ2IG)8+S5?!Av5>S%i;p0lNxoQAdT>lBwdt5<^BBc z{%G}Akze-3dFf8y4|7^vcuzWTbDF%H<#;hN^v=j*FbQ=fmXQgK%bxC1L~r_7+;T<{ zuLtc)v~L6bfIH5#faRsN5YrM9{ymHOY7Ru8L0L7GKZ0AcC@#mi8paDw6`kb@ChJY| z{DQnV|Js7=ON7&KDq0nLK|+0D%q9Fl&+9C}y?%ZeC8Mb<nqpd0-YN479tEupaR20f zz3RyYN8`K5pzp19CFDlb0zw7d+8bseV}#YwQTI$V<54|}^K^;9mmLkk^P%}%^|Xw> zt{lno$!3hz(-JTVPFRu)cEKF&tL|gh2A~V7S%qQz_~DoDb^wjy&C>5Y!K%H=p9qNn zef+DlsOD1#aoIW^a@wxKH<Dq~4?+u{^3%Tf2oiUNZt`?~^NGaIV@?`KWzWFpZXUdx zMk`ZDzZz&8_C|CZ(YXbN`=yt8i@30f$6syKh?T)BXAhW148cB?fZg@%qGk+e_ta?) z`RRHZgGHH7s=p3p*vn_x`ByNN7m;}4BI+*ne|!008|v@^`B3=Vb-&Q|C*=<Z{sriQ zN}USjpxc3}(y~*7?LV?*Wx9~M`QJ;-QVr^`GR^n|Tv#Snf`snkJ3PdEBWbmX1L2NU zG#0a!nvh!?gKZdROn_gn*he!!8RKshuitDk1ZCN5bbGo}fY`K^T<pYPrA`OwB?CZU zRU9LjM#lt$!8okfhjpdaBFEQm%V#Klq7;rk6V;b+KpP)7zWJpkFFQ#an408=^^|YJ z()+ICv6&Fzm3NlK0=*pA=o5CdWt5qVGnNyM??Uz9<4a-nufHfAu~~H*4fVOG?C+== z0$xmapLu@J>E$cAk(M_DST%4g1&i(X{22N=%`8M*j%fMQnkad8<S<lP@sbDg=Z9GH zJ>BsvWYb*nN{X{zEDFaM@0nlA!S=;+b)-OWdlOgmQ)sWGlYJoAT%0@nGY`8U?6RQ= zZ-|>L(xwP(JRT<aqbABYMf$BN322!_gN$Lg!XEM|NhyW`Zs?lD#b~^^nk?<r$m{wD zGXc}j*u`a~?Igd|cVLR_DC!QSRPF^NpR;h<rRS{Z@SL>NRuXffGD4{TSS=Tyk}%|J zXmL*<-=Ss};>V#1xSfcOI|!UBHSoL^kDF4qR7xR$J%-In9GUhzkmtIHwyzl9N`TXj zz)G7}>1D>hU9Z(W&?C>Rj@mx+FWZQqNlK2rvtM-JxBwMr6l+f9u>SEGWTu15J9QtM zHg_KQ^H$*fCD~ROV-~O^mO}~uV{3g}<cu!I62Dg$Kl7_XED9lC`8~d}b>%+P)UNF2 zf*1x;So4QbU*3kO+HBjjdEWjotzZo=A*C$cJnVOkxoR(2u0Rp%1EH*)K1E1()VtRr zx~_Pc<>z8$p}eG{?=1o>8j>os>UYs=l`Ss?KTHmv6}5QCAm8>?^F=O3&c{|M+49k# zr|zq3D@|6qIw-NfM$o$6kz#8opBLNIApdU40lUoIBoVv5A8s>D(Zr#fWlZ3yhIZ4k zsR?^Y1>VV5t_}>5%wa-R6e)Q1TQqEjn#9dk_ZF{*zoP64c)anQMYF8}N*^8GDX$1r zyuwn@1I5UGn4j$1XeCh@d#v49-enH!T5K<(ZFS`lKRXF)FFm<!ltj86?8ew~QDBo? zftkL`@3-h;brdzX3E7CqP@zhwi)U0pOMSzs`%#bRdwf59-vrUrj4|tNi}S1HAdfVp z7a5B#7#&(2qPkTQO9&OR%<`3~zVB*o^o3BQi!3!z?g_1wD@s__mlVSlAuAI-QU@1= zHR_T>zZoaI4|Z8nXRi@`f1&o6<wf0iqQf4?gJ5ZZ9YO5oe5|7Y4nxL`<mD7cq?*vS z0(QV`m;TOxrm+=gNPN+Y8L=0;N%;y&luK?phCdfH6B}p54X4OdXM0TCma}XA2)d-x zSpP9hqsiDxV(#mnz?EDf*qzoSK@z%NCB`rI1*2r*2&R=XxhCw?sLR8NOuO8&V8Q67 zO1@8~W6GC#x9#07MR%5|t$D@=1XZRLeX{MkV=d&wAX=ClG-O7>OwPrJHY}6UeE=MB z_;Y)@v|q_BW*QVqRh$eJWJwzmQq_h?spy~=a-6f5-fDnZw0{wO{b01_QNdHlwl-DH z-Ez{@X7^<`wDQ8<fs*VKQ=OcEi9JjTUm(MN(-w`!6ubTH+3#j@f=zn#U5b6O7B4v0 zFfGcFt1d$=rD*dS@~8-xi*+_}p*;PRy=(`GcU9XzUqn=Jer+hl-1_X!(dVXr;l>1& zp55PH_gn{Lg>-$`J~eol7AUecxJ37`68gn;fz_=R#J@}zWa_3@m5X#Gbu0?2>#qyt z^vK3nTH*MvLkw=95ON#e<%~bzJSK7FrsFc)mj-k3j+M22-Nf!#I4iMw3(ql|Ns>Jw zofK5EGX^RgL7^MlA^gZb^ZnI5F?*HaKmu878X;??>#KGZZ_qDBB^Msx<2@YROj>0G zl*eAN#h!{`>eDwa|4){|gsWsQp8$W6OZ;MTnx@+q<{V~<x>2S5EeN9d<+eqV1=5_x zvkXg|wxV&g4QTF{CFqe*)a2npO$7Aa&wgCL`ZYBQH5laFbbh#n>VNyn*!|wb?;4B} zRL-5@Et$6Oix*j-A39u>hJoI`OnH3aP5t4WJ^R59Tkeh|7&9SfB&tmthJ5UxCO=@` z@>)m--UF&Wthleh%e-?+kpQPWVqfNT(aWQ)bB_H;;IMW3OMu@N^97qv+d0Bi&I2kT z_v`eB<E{9OmkVY5-enIXV;{i^;#iop`}KP60zAxn%N-?uSl<A2p)tn^ST)+a6af?p z@Oh#Gu@^0E6q{f6AhFOPdi$z01CgWRk4)Giudm$XURr#9I2S8y<Q^M)2!DLQ8Bglp ziMPR~gyXLb#>SP08GU4EeCKo0xh8aJ;Ze?YcGn~B*XxI`8;ii7D%2;Qow1NX>E$jv z8^fsADf07^^sE)Qtfk03k;I>dBdy1r(s<=<=fJV(NgvJcfCuu&cAv((KdXt0tFZa- z`}^ZD!IXy<>c?iE#>XQp8N|j$$;*|H`;jywU(Mr!h(K*$*hwyRZuMQ7N9&`|z@~h* z4)oyhU`Iiy3~WuF8}=zv%NN&E>hR4m;5u}3kW84L5$DlU2pV4K5-Lg+!+aUC`+Xf* z325tt4HKeLnH&(;gI%MI*rIHHU8jz@0dw|FT~i71cm^UB&Xo`?5%aZ*9_Ggcez~Le zFh^w)!2A6OYl)xjha+hAgVir|A~@0`+c=DE9v?`X>GcsC23y^mo-z|(W(SRa^`;T) zM$h}cE?l31OIup_2=#}kNyxQ5rcG-@P(3__G84KknIMwB%3lf8Z+i|vk+Bl<9Ng^u zuMo^6nygH0QF=|=gBkkQM{>VsyS<EY%5x8Vhu!J|`!tHfMJ2Me&C=%6YZ-u9X{s)k z0Vp9sXvsQVqZtQ<@|74sbCifnDFU>~<5tFPQM)6@)0S{(cS-iQzS*7Mb{`Z^2~?vJ zNNO>pO51*a+Zou>(k%u{$56G{{ph~-s_s2E9T9boC`k!Q-u~xr%V`-@=5nQ|ls_Qf z40gB4U~v_DdxZ_AXm*XEF)g3p0S__&o=59<^!ZFyVYDX&r<3xM`oX?cb(6viS%wtp z$j$kbG^A<45l4yeCucbmk@*jhfbLsokA|WVE>`gTQK~?x-Wzj4e(KyqC)lzzA)zDg z0`e~O68A0_F@Mb-X8~DwV2!>({kXIDarL+khH0jX9~kx+Llwx6QiFmkuwzk+n2MCe z6JAlfa{jvsl&kn+ICt6CJ1{X2+jGsKP}OAP@eOluxb_543{TjJGc%&@_Ws6Z4_THQ z9AVwb8Htfu#TD?F8U*iPKUt^$m1_H2Zmu1^+=ryV#LERtRhbV=I&KOB9IU@@5Og!- zU^rd$;|R)M7Z@nGfn73U7>t9%-F{K89+K;Nv~?-5R~cI^f@^DRO*d|BZR>-zHv6xC zNyTRJ+6^eAFR-Sb=?f<U=8S;#*+o-7D#n7Vf>`}=RmL$L5=TGYV+@o90<@{Aj;Hjq ze`;H$?7oP2kDGPKxRNyBJ2|ff2RvCgg{@Mw9?-tgx&MPdA-XsQ7Ad%GKGfjlIQflF zW^u$4K_ge8yeJm=hXqXz<va;p`}9=sQv`@fil)ys<K^vXdeIDoAw`S<QmUFNF3zCx zdvzQ|3b&sslR9&Sx^*3g(}+&$#@^%N_f`y`EC{F`+Nij{xs>a_ckf3#FUSpk2P0Q1 z)chJ|{zc1D>e~@|>41CsR+7?rdgFu_Qr=xJ<fG`Rf8m^JtlG|IYzjJwoU-?-t$cs+ zS`zuLhZhLx&6wk-A{Wx^S;u4O%JkSbp;K{D3cM{^z;H2WZ*<+Cn*~GOo*YL71H;>c z!6u{_XQ+>O1nxUhQV@vzabFIP877gmqhu&Embd!_;luetLlG_Q_=jny+=$R`MIdN` zv4uurpi(IHg9bAGr&b0nNd}QFexe~OdD1=etvjH7u#V|03u@#xHC2bj8zDw&YJU}m zDR;KFSqyt9q+_l4v{Cvqc+UHw>f$OW#h&!s9ZDV`L~)~KY|8Te*RrWRk+2s*bPL-k zO29Qvdc>*ZxR|6VJQ3yLK{=Q>CQ$;nB_0buy>1>%r1XVg_9crjo>)H)6gxmMFxY56 zF2gV*`JHUi>|>_<gPl0aSnzrr>%11PgMyix&>uM=9*8wY%*dDVK*EqBS_!UCr&V?G zF^(6#jffAvA7;NnS2aAQ4PkgtKAGi6=ZR@1CRVjzxT2~3eV_yJiN#_UgrsSJ?dEq7 z32qMOrtMsd#&y?V#)Fs)RG%JamBPXITvw2~aI|%D0sL#6G@1l3;(dMSd2vLlIDk}1 z;S;XY-+SatkO^!n@j~`=jrkd76=k*Y$OIv=8D1ljeu2*agZKJw55`#4>c`baCZ6@h zRY@0Bvb#R|{cUOFo+QpCd>bzFQYxcG^o5RGAv?m#pNBWnyoxrNg*!*nf2M|Ke!ij= zcAxoqKi!s<I;L@P#6}Y#oPN74^)2YKaOrTLxMvmVXnnO$y2yoZVL1~{Ghw?W`oO!m zA;zg|`sT+$n<X2pG6SZFUv@RM=du~n=2E*Dz$D%b2w{+EOl09!STT)tNp9;7YN&%) zdtr-PHjc(#GLLFBu`6H+Wo$K%JaJk$*tuSpNumC*{932fir27o%?^N`(ye~9q1Y0b zYz_ZjiKZigc=RiF!P-=;vVuLbrB!Gs-?Ws#o7gkqpYB~-I528g^0OBoF`I^d;u?SK z#=t5Rvmi23ZH#hv!Ta!45c%ru?BixaI2i5QTiEEz!%y@oRyrR&xH<>bxJKkL4lw-c zi#jF5h8KVnL@iv(WKNunj%K<xwlgF2k>ki>gjM1PmXGtg_A{K=Y+0^RdWW^&$@YJ% zmX8x8O0~(>->Jbgv$`=o6`F7YIN%}3@)FEV#tI~<LQDs;s`;Z%uZ%-+mL*WN^)4cH z+LF3|S!g1jD2g@kY>SoSF4oD~naUZK?#z8&Cm^Xzmo)L*bHv~x&Gy@xmb<_pp*iBn z1-B+yJD@O|*{5c-G$-0(klEEWM7jsvY~blAkB$!W+x5fn%wIaq{$XO@PxpVbu!V#H z*(rsG!_scauV^NUHDQ(T3*XtIdh1J>HwcCC+BmR^63c3Muu|ja^bh6ov>5!J*0~;j zw_~xcI2T{#Vvj3vF-fYEp(e#Us15z3$Qv@G#+joPL8o8l!>;d*y=PSWP4uky`unbR zhUs$F#557?ZD>zt98?Qg<nfeR<D#tUT)$2>6VMhW01Qg%b`&K}*L`Kx=?jDupUq zUjFvaca0_56~#iz0w_h&O#5Y)D+zDeKqx+Kf8J;1f|Y&|b!@)T&?21Gc8^?jGd}3~ z(PX5j+nH^(g8m4<*`Vq28#nrsi}eruEH9&&i$B~pFd2s57x2S%UKU!TVrI+V11mit zoZH!pspmaoiWrl)&fk{Q$_p(2h&;mGNQO(SDZhP5hxa~orvPKd;S(ub>`KOhuv;35 z4(Ao>J)7&KscUr`;tJ7_rT_wZB)Fkcm|eP(w^Sj8#0)$W>9hB}nD#YO+He%vVAj{t zVEn}<Ul^x`R>Bsm23jIjAY-TYYd>7gyu5{CE2=E=`trOAwJEnxD8U5VM-AZ^I_U;J ztjt|{JY<EAfXd=_N?_+(dJii<nVEjm!t@S`wwXYCM`FR+ofI;K!J%XH870PgGR&*{ z_@Yn1xob5%Qqb2>`FEmLQZlj&6BXy=k^xS-w=nkeAbs+KB<#<bdr+V*iviT{%pDTI z1+Qm0sYIA=(6(ru-TGa|I8tuYA|)Dg_JF-qkRf(=n~=AaH>{w05v)gzV|b#=;dxwj z?mxj1)))1vG~~yd^B7gf_ef*FjCVr>HvT*8JIzUf0LneKuZ)7!e~LaD_*mBWeVjn< zQ-+19pGJVaDk^I(K(i%olK!c)t?Yqw42`GN-DT3)MIYj!`K2lWxsM+uv~9ALI<MOU zAMRW9XVYc#on9#T*FJ2WIh3*q2zCa{>7D5#?U&|mY)BKd$XSc6L+G~OB@lal0%dBP z_mBkBrN>PNiAyFW1k#fzG!orb5+1jS_rn;E%AFf^BinPGi$eH~)cy!o&U4nHHY%(f z1Q!T<tD;Y_9%TgA{5cw_54oA(lp@dDY-GC5OCKSA^<G^djP*kR3BTgR@S=Zx{$?`( zxHF=EGxhNzJ=8?EMC1!%%~}l0P@xE0><9!aVghJ4*olqdk+Qdvm93yK;E!oO!vKpN zCa$3USsIi@t>Wf@%XV=Sw?Cvj)FY~vMb+N~7fw-^86}kZQWrEb=jE5^Kg&QcmWFR| z@^UCpa7A<JSEom%u;4d49Hz0r6QXY^eMV`5rZ;TU%`hbm*^h(off^d#V6US3l%uso z?AyiN3|B68*=c9^z3+~Na=b>2ST`_jA#i0Aq38<5cH?HXP)mw^zPQxk)RAWpJnH(Z zv5=)RH#DMJ@}VDz!^yxKG%CI!1y+)m1O^pgqxm#Li@7R1@iA_jj_a29%rc)xN#4%8 z>~UQb30NGO*nE_bY0Xcst;pWd)Uj~beT92hVfnl1Oqy@oXI#^2c4AR{(#al1Z(1ZV zPp-rV-h<TVL@F-M^4Rcg^Nm!W6@JK%#Q3bo&vw>+St#VHw-A5-IGlD)c1}XW=1MzT z$PKV1iCLWJWUj)C_TuFtIbaYjXde|u{@8a9s>sy?NuXUN8C>bdKN?eomgS}W{Dl+? zrJHukS*C4FF1#u@(Qm3|7S)2~{FKkgNeJz%#~vu&zo6f}4QVT{KRBob*iH)tXAd2S z$sykkw|;Exrkp?BCjW6vu+UaJ&cK`2s9LKlcSqEtN0r(>hEWi|&w6GwB=`-Zpu6Z! z=^`!K?pkkx7>f6yxPNn@S{+^7>!bLqs7re8?^6Y?;yfxHdg$il$@osNaA(B9TMtc6 zQg}jglcIUl+oFqLfRa}Txl@>oz|o#mMiTpOu@wb(fIJl6+6A@lRgH4<J&P6r=m<Xp zG1bNVT53rstBRG8I29z@WNAQk)A}u?9xEcc%8<{g&M%68JXs%?6bUs;u?8i;)*dI$ zq;UB9{kGAq@<8h%9vva<Xp)2xNiokX&>n~UmpYq&X{xmx925icD&$Lo<LTYtk(uJd z>sTZ^ON53?N0ftX+EWnLyv*4R<&|Dxnp&_JaU8UCvX)YdA=qQMm}s;k3&>-}n3}un zx=;fg+%m<C;&ijq*F9Qj1GK2d_|+QCw_Yj*+HU=kf$^=6YRSSZ+<>{E)Y`Fzcs(ZG zkj-!GEYU4~t6vN>Z9M#C{=9<F7w=|^3B^_Uqbnp)S)ZT9{cNpu2w#AB+6-7J4VMc$ zrp#D+-X2%{WU@G1XX>G?!TVvUs%$=o)DY`MavOsqrR>2t<Uu_~S7iw24bJq|NC|=& zB{Q=fg3`eY90V}#NZPW<l&IzH8IIFW*ihV6NZEuU)aqbRzZMKv65<HNm0eYe<HQ~I z`^>dH7CjqOl3HEyc~|%4@f$t<9Qt&7b+*{SLr3HdjvA3Ecs0zhT{zYTGkEo*Z`w4- z{*rZ-7z_*WJoRHYhW?6}S$>)#g3`y~7hZ?!A7l`r{4y{bW`w;}A_00KCYDR2IrB%~ z_d>MyK(%jui*QA!y0WSgF6c!DtV}X_W2A;_DhVA?kMRCb-*@7&>_+S{L%SpV=rAbu zH|JgU8v|M`i8sNTd#wzqTn^}Z7%|~vX)Z6XTq$+}qALt5_}MZVH;T88*5tMl9kw|6 znIJ0sY#uNrT%d{2mGiN^YD}xSr_x4OQr5u0h5!548O?`D{c_rB9d6oHrgfN{G|WTB zGG6{U6wEe(CKk4RYOJlKD7mbA*8G~(-)0;uPT71KzfRF%LPpnktU=v=#ul%;L26#W z!moxggO@xRz^C0cS0eIw8w2Ti=Bjua*FF~ut;34H&xF(k0zD4bzZYbEUNhF2YWH(8 zCT@^4t4$=u%wQi6@Kq6aqY#^aooKw^`lz8GvX<V8v?H}M%+Kwdyje&5GF!cVqu6pK zD(~qu)<<WyZm!8-U5ocku#WH%ep^%jT!01LsWnA#mBP{t);xwVd(5k~Cp1h1`SDG9 zU}PpwKy?ws4Cyd3+<!;kJecpfVFSSZu5(*(ODifc2Q#)`lb3%>soEBeJTEo8YY^v? zdLY}pUyDAuv8cE&73ESWq0}kghA+C&uT=J8kD08dlwAjX>kg}7^{za9_08IIhWf4N zx@(j3=t)3{yW=;_>k%FonB(lVkxN1hY=ob!^C^<f5wcE<n8j{qO<xRC$NRJSo@-9} z!^p^}wSbO{+(ujq;5yC(R>Nitw0#&)xo56$KM^NIDL*UP6h#D9koAtF95qH|<iZxR zYD<{!_$K#W%BiZ{w5X?#PI1yyW;2(6)-lKt$yI(LLf%x2sjQk%ju#(DQ-cG`=OJO2 z30P12-Y@e(^;A4;e#7A6YHB#eXa4rw68m!4z2r+4Tnc8d49x=7JXdVwl_~sJ4k;vc zOn8}++4ba1&P63+61cfC&7p_+TC?LiU&&-DJS@8Q2f8dQZ+YU<n|JGf;yEFs9q02O zK6<am+6y_Vj&e{H3GD=il5B5?>fjR{zY^uj>ddEZ4t%L1o_}|JW78$D|0{I)@rCip zCsC`{mT%o$t<0RzpI*H&w?~Ka(g0}wc>&@BLTUr-=IN1DRb{j^6lzVQk>HTQd^|KD zXsu058XmHurnI_(W;|-P0|JO28vj0nx;8!=M)Y6)@g$9_2%g+t@mGz3Ffb2~h{%6! z<e8qK>*c9o)uMtKgpd@W&=$@6)6LRt9D|LYp12Q5Rd1N<y`92botu0bL}AKWMfp6_ zab%WJDYY)&?iDc$rxihv1Rj#Osr7WT047&4@OR3@nQuwa+pN0+@k-#nkM+(VwftTB z+YXN#&Xe~|>GB@VuqMOfgaT4h_8sAr>l?X0;;%pKP@ZL-zM4;elWVaMPaBNF8sB2Q zB6>mPw*OkwgLn}V*t6+6T=q+0n0+fT_bZ+J?copEsh^yNO{U7Xf0(ljKX){NI@J@> zG?Fso=vjxjN8;8*ukzn;j1g`tZ0*$&6Us9XjtQLwX|nkU6~XHE&(4Rw{-n-`=OUDk znB?2i+18oe`dQGaZp<Wa60eb(l^Jz>wlz0-J{e&z?`!2P<7Mn?MH<@UW$Usq%eYOL zsP$=|5DcwZF57M<jc5bkAO%b3MyI{HN)Wlj><Ft(s*MFk*2dIk*2dL_U$EH#fAWkH zjpC0&M%70RM`7-x3hCdVg8bZXGuPU_>h<f5>UHZ4-XQ%<PM=A~93>ld8#PMTYtl`Z zPX~AmQ{J?(wq?X0XT3~URBkxSdW!q}GQk9|utcLMq|hnL{dUxOXg1+7Mdb6VLaJ7W z1I!1^-^=XB%@>&;PmEkvBY%^g9E44kSm=l4eAoT6O#>t5l+-|M9=_PGu}zf5prOaa z&Wnr^`#y_ymz{hZvdLPT9*uiyPb$n<t=*iB@Ikq%Y;SJ217!Krz#(-$C7bqD<M^Zi zmfVcUmrp2W1Mavco|(s=n^sZ8tC07BPj72D^fRRen(Fv{AyV`X3^BFZWJk0mzs*j& zH+8lDg9F=F{qQ<0vV+vgH{N5j+)tZ~!IWW3Y0=uGjD22=S9=xDMs{}-WHUhO8g%5V zlTgj~P1*MxiraG>un~21=u^Ltplz<^pE|!_;I>ukdl@#Ihop~CH!1fjnefdI>>!B~ zG>@jGWm-08SKMVd`rf`n|ALE#s!uF(n|sUEiUTl2y-XQn_EG~BCW%eBvQRS#<;h3o zQ(J0W@i#s$SQVA45(P0v0rMn${n5jlDyT%+ly$?7C^D$ZFw^m4Ga<}tv@CR6S3b)r zs45z1!;q8}CYvD-4k$(dJo6e|$)a^ZLR-ITrNhhSNLybw>o6P%6m3a-SlgFPjXmzO zIt!c5Gy9&9v|tgeY-{)W4E#XqGAZ(~nWdXyG@{$ZftaBfXQOUVN2H3&#yvl%+!Q6a z1o!h(hTW-nR}ma#eLBz5O9U^z<UD4^yf-Ef7%jD}z{QSEpXu3wCOCLRgiP<6ml1oy zsxNLDzJ~7}h?jbdV-XEGg{S0D>`(s^;EaO_Sa-i@#g#yD7JqP!5A{8(6pOc+<^0O1 zLeq;?@seya@5Yua_39h@!I;oaK?nMuZL$x_h6ZO$X%aQmXI6t42(vFf-)ojFIQe@6 z^lbH|ul35-uzH)`S2WP#(!o8-EVYyu`9edL3g)8^vBW7qcX!#6q{0!;ckSD@2enMW z#=Rei{reVbe~R`i=c#YjFbrTDOA70Fx!^6bU+-@>?o{KfjY%F#)^c}zAV8Z443qj8 z>lo`qWNFj4BHTdi(qfVq^JtylOb`Y%5}e(UryeqqC#+ay7(%22V;}C2qyo>@uBUW7 zdmKx}n0XIs{ZvcD3*UY=)I`iB_`WX>;~k#h?~ZD58ehA@%0<GW)U?pEnQ#!JfnScM z5*K}R><K1rIAZzEUI?nPX(Ut>Q)f?(+@FKL_mR6zbGyOUcT!h<Q;LKYCuigE_6^74 z8j5*#yX|s|xqF0A7JhqMUek*(!e7+<6{ht!&d`S9rSayEWIP8QO*et*wTth^VT$j| z983<ZY<gGbz4C>(?8A;J1KP*S&9kR<jgZW9XW4sfLhig3S{f?9FB)^vzv~HJ7JT&2 zesjiRoR6K+=5K8x93Y7olPxRjd4{q%g}6;*2i7Eb_u7hO`dAc@?sJL+saRVt|5?eJ zhkPEi6GR5VGarP96dZf;v(o-1hY7Z1$D_{O+V>WKTOm<f#<D8ZVpE}amXvJNdJ}p( z1Fpm^uH>el!y2+$CtM7(<`fHaJI!@bEo|*#?{>VX7AYT7)_}g_zzKTjua})T!ds{T z@uy`%=q*3g^BFJZi<ri?6~Hta%`|e$Yur|MO6ai!RmWqn`!Ra7g$aLom_yEt4Db8d z9X32%aB9EL(JXQ+b<z91q*<4h%b4@=<RYY%<@OEQ-C*aYf~D0tPwevEpx1he??8Hu zY7HFBH-51vVP(ntQWOTYHl6KyyQuH4HoNp)f}_kM<z$DFEUOi?(l`r$*d)KGmInTS zwOq8fC$pF&=b=q`HRZ#WVCnEzW==KavqUHhXLtAacm7YGieHsZTOl)Q0a}?58VKHU zX?6JKyy4$s*4Qk2J@}*UIvL(0Yvh6o_lS#w)*hf{_2n~Hpt`O(yONlJNtWfQDWate zAg%u8-I`}sgWoI%e2$dh`b!8Kx{j0DZh(WE&IXf?#78$(PQC!GSFjmfCHK>S;r$v2 zZX-0Z>5aF{M5j-GByk^F_rV5{msMg@%Zk})=^(@|j|4qD9bBHC(V{i^e#33c{t%(2 z8z#8dd;^PjyHt@}XTjwXP0+MwyL4rXWZVbRrkO(d>~Zp>>34ew_)lWCCJ;_eH#9a& z;Jsjamc+P+n(oMVu(wxn%|+U6<U+4uHVLlVmqgU})mN<ALvu&SxdAKWn0iJlk_jH; z`z|LZl6!Vo8Ky{gh?S)YGc%y(PruNjTmkHadTH)+NeI;y$J73s%e$4QW^C^6O|TbX zjj2RrnAU-PVJ?>q0@K%cL-GLrTh^9qR-AjP41E6IA)@V=Fl^h<hFjOXI{Z>560-f* zl>F6|@^u}ywNldB#-1}8$i3xQ<=MPy#K|N34eG)sCcC?EbmL`4owC(!eo965zzElx zt{3>lc8AVEi-2~z87?ckf+mKGrpxi*j$vi;J@(yUa-@x6JceC4hDvbSrFAL4kDeA9 zu2=oC@O-rkY@_6?j{r#;Dewn<o}5o`sG9{hDn1pxUM?_FK1156n?b!f=cZVzYQjOf zpUjo^F4I1(geW5Dt+KUY&yEYR_sjdk_>ttyksn44MF|Na+|D6g`&U%&9h$tjaed+@ zwHg_!JiV;VsBm*P2I^lR>W^A{Gj<~%f+>qF+>zoM!Q@%UOU!lUh+!y0rPM(BEB~|1 zy3XGXo?M-jB!~AWIl^}C+{YY}^Lxk@v*zV9@wv=3x+1M4Va<O|1PNulgwqJf+IX%h zjl$SBJTMNGuAx{2h;!3q3Hp<c(?>jmzs!AtbIgfbg+}tf`+6ba8q9>=;@qw7HjCF& z^xB}nU}1Z4W5_Mu9Z2oE+<C4rw$&Gc;Ws}O#;A7BJlsG1GSFOl%NHqqW0j(c(&`w2 zz&VbpB=T`7&_<k2+iXrQ!lChvpyp|RvWag1lZSasTRwJ9COHB@p}u=OvC79W-06+h zgMIr%Yoy)qQtfv%WOmg24YiMqSK`_OqvkMy6WI6Ms_}B1&MPPu7INM~IWRWTy4Fw? zuDWGoez$v#+IuD2oW3YTSsdrE>P;z)dgnso;SatGW~qVw8$w*O-$63$ERbk!WQ=0V z%^zoxc4K{GQ)a+0@qvdR?jEWrI6_CqdfgA2kqh#Hx7x%flpck4u7r$Z<3ZIcbaMiB z#IPBxcF5t>xa>*m(X{=z206()+^^$Z{Eo&TpvdR`)2hcr3oRbqu^?k-Z%VAQ1&gV( z&IP^A<oJ19HhdfA%SwWk{)dl0EpFE;1_gF!0?M-~^pDV9nA&fZakoee5W5=n5?%YR z{Q^$JbdUhvq#qvK{juI<NkaS1QJV>Ih=y72#iTB>6~k-QPI6<g2lR=xeZKLGp0IXq zt-vlyM5hqxY0Acezy0!BY_HGV=ySViNxAz<K%LcaBxJ2p(Rs!Gm%yO&8=ZXeqMZr% zgc}Eahia~eIa0Sby=Jbvb=HBIg$(REgAwBBt~N@6#cFm{-7hMUIHS!DI+b>V<RGvW z^IF%K+43$&2uaQZBu!qwC258Mta)AKU^^+P1HLB^fV#7wW$*|*u>0F&gReTGov%NO z(P=8)(kXi5y<CXs1g5qY<3%<im-<84IYEMUAAHEzV^G{Gh-3otV1C>)Onu!hRA2hc zgyrDnZB-2{Z+i!RBZ!^bl7j13N?{n{r$n)n8<ckL2%jm*EGauPXS2VgEYII|L2}S; zKI;?GUOI-ozeYbl+03ag*2WEXnB8<rZl$ov3Fl9Mof0N}d$_YWoD3b~y50P!x(_`H zT^3=Q{Sf0Cf`~Gn&P~AU#h}iV+V=qOZgDtcc82yNOs99ehq^wbiCI+o4GcCEd2veN zcE1Fb6Te64#5y~2Qaa)Hk?`nR{ekQrRpuu&oX-l+NNcBsbR{Eshhr1s5ve_Fll&=! zOkbmKMY8Rj69r)!=^=76;SWz=yn&eQ*SpyAUtdO+QAVV6kK@CKOD{YqO9edb*A5@F zYwkXfDB0j6h#|#{{%$?Uxt4^{9?!71dCGri@pI9q)Fmbu4Zm+4mm0c@yxK8;vtwac zP%E0|^Ljb4RyM{{_@zZjO4VX?BVD{U=&pz+(7f=+^7hqnU#niEfU24i-PrOn_dWcw z&-U_!wR%VcDyF%-ReiZkhinX`Yub5l*91!{kymsC1vwcB;)cW&P=+2RlZ2*oyzlfU z?;yO75bF;tB!sm~M96mrwEjXueth?}-5D4<&{ZW#&D^M;Gqbn&jo;~belJt5n30GC z-h6<a?E^S#Te~914WGXMCk|)h&<G>9)9tbA5-%v~I0)El&>YBJxl+ws`(mtlkdl1) z5%2f?1g((Q)kh^F!~=a810mrCx?X&)@DIXcIujBVyzAU~5MAZk#}Sp)>Q7`o(ejde zy{)>r5Ci&3?hrC_8<hz)iq)Ru$4Hfq7SEAcgEMH_*PqTu{iPNbD(<cmHN$dVDSS*6 z28>@)$m?Vx3zVgg=V?T03M?3R7TX=s1%oplz7Kw%OPGcw|8`J;v6|&LuY7I(SZVG> z3(8xb80DAm9|fQdjsu(cbeHAh?daKi-iLOZxeAaJ4$4xIlj=XZFO#+jjrM8;;f^#h z?5jc4K7E-K5j8yGxU{Vxe699U8Nbu#(IX4y%$1g*Y5pnDzs_&=r<tR#U_<Mw1jp#r z+fDA?PJEEtVunZ>Y^eo@o%5{7Z0hYRjZAq(Jw<D+4b!xhqxzQA3QI)J?scy&CPmzE z3eoN=_(*APgW-+@YaVhQGW-)0GNGuvKKYKA%=x7VYXld+RWzmye{H?ppswCi%nD@` zvmCg$XynTIQ|Ne(9BPFGr{D19i!n1xMm*(zF|4%hiW%zRz_fX^tfv;Tk)EELdH+_u zW@7hS2ZL=WS7!5#N?=3v!qMAL*uMco&hD4vk9rvFVmM6t7TPHUC&sf_Tba8Nb(f(7 zF_J49F#4@Y#!nTVJV`U}@BUnUX%DWstB&$qtC*Q6YOkI>K6bvFhz|{o@hAA^P=Ed1 zQ-)WU)3iF(V;r_9q^cBEqicihCVzFrHa0EXn(%V_=k^YJxaMW50EmfXi>hBR{r4T| zAZq!+h%9LZSKNf~Ca3~(kfYtSt~wFtL)k4Ny3n%fv2)@m+khSUiq(y;9*8aL_v(Hp zX6qHeeXjF1wN%}tlD%L^PvSN}zLd~k?Q;{~&f%_moD!^vr(_w$F`8KoeS;~blQwi) zflp(RE&i6;(s!+wW}|xm@xtUsYJIa`9cWT``zX<gG3M20lqDTjhW@zpN~2Y-UFly3 zzP93T>^j=B^SG{NAeS3+hIMqkl6p~V65IZ5=5|(I(yDD^bG9Du<<b(nF&Rku)f<~^ zom_Ydv@Mjo#t|Wsp}+4}vrBYgEo%<PzpA`!r{u-!O54lJOH0ek+u6vR-hBL2GLv(y zUe$<~7;^0x<MGOIF;Q^PE}jTcqtKmSL!CeU5ed#2CA0Q&pfCNuzWzz>w1R6wcx&gG z>~0O01OtKi|K*FGU@be%mpVk1g*hwnxY2dOax_}j6N>oJ*-*WxaJ+EkTvUHk!?0Wq zE-|oyB*Mt#IL5S-Z7QYzafr2@wm4oQ$(${`0I--RR&6322(<+XD7zZJ9eSI-&oelf zBKmgaPUB>z`K0x?@9#T?gjRCKIGCKZR5>;dnjt>!+O6m4-p`%O<bW?uEgk}s2yOXm z+bcUKDeFqcSxTAdzcw`z(xlEqZ^~ZE4-Q>6O?%Ns%r|MiHg2M`6Z|b2`cisCEx*z@ zzVb&0Jv*19hxz0I1_FFCM?o=wEx<eOmYz`FDLbH8Yuef#Oep6g7p!`~N)6kWw})&i z4HiQa3=!pMOFz55`t)O`m9QCF@b38S@{;h5r>57BysW&BIh@59C>sH!RKP`QdF@bj zAhrB!E7jnUQ9o;usU;p|0p<^uq4EttLlKqQT`gQo-Rvq1b>3vp<=d3+rj`V~_e$sa zYr_NB<d<#TDxR+Z!#A&-E2?1;C(Ku73sP2jebZZfFYXsA<b4Dc@lMgCP8~LL)d@Ch zH`bKG9tw9|<-yaZGrEY`RM}D3KQ|NyJ7o(fM`@sQegcA#dAd2|ePx&Hn6l>-#V^ip zK6If)ocktS(|;~zd_8xVSU}kSiUozh1pBkBy-^OCt8)wEw?*wY^;ajbnxhq5@<ydT z67*kW#ytdkKT<yaIPV}_rO#?@2)Z_5j2oHk-t*WtB;G&bJ)Az%AFswCS5wS2!-*e= z8>4WeD!!rUGWawcs;ll!nZfU*J75itN46sJ=7t_wS%XW81nt?ENCWn!PIY`u6?CFl zzqXO`O|deJSnSZVZYx;91bU^?x!qqWD??X1*xni6N47!g`3kYWG*3HP527Plcfhlq z`XOKgu)9ZdkZpM(@Kn1KPB!#-hb%uRa<-<?TBK0@7>jbN4oPRCx{;cuKEO7fZq!ne zxc$C|D8SFqeJQv-HwUiS$2WgstRFCRoF&@Ba6^`<)+(9^|8=?ybMy9DZS@Pr`g-y8 z?rY1<9dT6Wm@lD7^LzY`kYUcipT2f61K1{Is3HtgcimoAK(GEC`nwPgXORThXS#u( zz!bTwMsf*ctmY3~TN_>U<V?(|4<cVNS@DXa?Nv8-bFB_~F#2P7dzCY#Ys^AVIncz- z+2`M|Mw7J9rSB;f!!8(h+CDnwE=l_fxQ$z*S_QKphW7`BY&AF)orkP5q#rH4A8NAX zGAk3NVC!X74AqUR{1|)c=pX7BP$u1;!Dygs2Au4qCjW!o+cU~G5{{3d+a1tHEjw=U z)xps|^lit?`(6A6U*EO`S@%okqShZG&I8`4r^K=%x4Pw5@Gx3kTA?0$)tS`6gj#2c zQI8Yh;OII<O0C(}JHJ)&-31%6UK4gcdS&W%W^uu3eT#B`vXC#R_EGh!fp6N~H!A9f zH&)g;pziPU3JSDlV*6uB#F<ROEM)^5E3smh=DiMg5_{t76@BcUKBR?E6Bmr{8(Pv6 zR>sjp6HLbJ{f7CbMTGv2tEg+3@XhD*hJDpLWz6)Tiq%8pW=!zot5Aqkw()XZ2m}dj zZHI8)+H#3lsW{4D9{TaW*UxHbC`Kj&=!Im*R0RtB*$$?+2~RWnd{ami;mJwgak3(g zwp2dqfGr>YHZi?6Tf;Qw4cdvxk51c1bB#DCPTjm8W(jNoEmd(wn~Q^jH#?iH44qus z66@D^l+(UU0k1(uhaJDy={Mi6=?)gC(qsm*S1~5wTY;b#*!8C)&Hb7K90QZ3_yM1E zn2`HEB=Zx#ug#Y*flF+vn6tH@sC-TNd6UjGTWjMw$yTO7G~N)pprVtUR!aThPv9D> zXFHc1Vw)SxbI?O@fk>&WfzX-s9&9LN+3Lu_4)#Y&J{bCSbGs$P8Q%hCqs8AaZRD(= z-vRcpd<c&wy1DLdjpsY!Mr?ImJ=mKJ33PW|F?$JRE$ta(rC!Jo*Fo@BRVku19zHO< z9luNynWqeQbF^Q8OFE@1d832x{Sq~}EbfpkMUMgYUHDg9)?v)6zOp|==#5+X2=!WX zb->keKHph%?h{Ba8{uK4iYVLSi%OTYci#$vx$#!1d7U=yKB-YJXg*pf9X1>^J}47d zP&9`ra2{D@sAS81Vp4%@vC$&ffLK~uINV!VrW?{@q+}pkhTn<r?#aBp)e5De*p6Hn zr-NExOPF+d0%{*3#JgFbpVs8^nlEd74ndr=#x2)T7|~f;=brq1ocAYg`muREr+X(| z4A4ouWNZ8aFHW+9*7v{5TD|~e24q{CHW--hI)7h2wyG%eV1HpC5GP(uoQe}6(ds0e z?P+N$SN%S<Sp6#ohX!#LmP#-x`uWZ?0=Sd`<JOfAFyi%$-mQ`!)UcEoopSyr^@EA4 zq4C$uN#JV|7TZ^B5F$yQwYu{1x=WeF<=0M!6nEKznz|iQVK0eLACA5%pBKT5o85Z) zQw?4nnSR3wKqG2{lrPmYh4PHX&t*qu1htHO-pfK)3SchpUO<(270_c|i=la|7#7Ts z2CEUYYdXZZ4>wt4DIcJbG_TfK$Y&^)e?9Hj6hWV0#>0agsJw;CC0^jIAx}CT*k08? zSpz$<0YssIenOb63JTd$wVbft5zfqf=Wf<7%4ACSNd_Dd%+K&PsPf=@Y&$Gg~d zJqso06$4WAQ-k;t@xeddm1Ky@HlT^q!3ZvqjZc`zaZFrE-zC~k(>qsw$UhXj$w@Lc z@GyBRYPw;<(#v74L#Jz}oB2n6cJw;`$nRa<nwF8gG5a4X(Gau4&zYP|ebMrr9uF)( z$IVEJ`7OI~($pNwxgfGmK|*oZF!$^a1M4$>d@i|G0^D?O<rA6sObSLUa+{-r$zkhr z&cqq?xoCpS1#{`z&F{8$&v?2XNqjAC{$w}KR+#H>4$F<n4a;39sZ0<OlG2P3U&;uR ze2LFp8gRv7G<vDkz)1G8E0INt*+7O`^x>vDUY0v*g(@@)aOSIb`87GIqg_lbqgv(L zC8(jUVN3tzcDe0YHfML|q^)<-@_X1R)y>u|%Ep(~$K;DoZSQvL?n%~aC0$N}3b{;* z%(WIT&p9X|<H0xCtmP~v<_^31#ROJV!-cPZwN<-T=*M<6LFzV#GaLz*XB_wT6&o3< zkp&9)4bV!iZ%}d?(cYb)pEWiA@fJg(Z-wRk{GM`>nd$x7w(otFBaY^5zQ-<i3VO?k zy_3U8jZ2968rI==#WY~CzjML+qdHu)-OQgqRREcjsf5NrmVMC~-#hn4QfIh4AOjzm zA8KJ{#mi~V&kN?{;jyyh1Uwy_<`5_tY6UO@Sy+RU*Ye<+|8Jh{`EXL`5KSIl0U)0M z5SWZn0LSyM=Q0Iw5&yT9E(_pf|8Jfqg>a1jC(p*>LO2C@6bKJ5knbtB+hREK|2d&3 zfeVE}fKZx$vIo$-ra}MbKMw#31pQ?L0C_<CPd}CZbNsg-00`g(0{-2`0|4=ZApdTA zx)#h2d}ib0=lRD5`_~0|_#xnDj!?*dIR2|2F8~7i+mDx*@2_A0KwcimvqX6LLHz%6 z?bH5%Cr1#F?_Z4nX#@X1Y><Du_&@#lz|Vr_h5qxy@;}FaqxFOgALK9FKkp~gl)(|g zo-F_bK>v;$!~=!?4I`8v%=fnq#KXh$_q9-70Po+3fdKrV|4JJ6-%$df05Ih51%Xfq z|KHH^L3y6T4Fv-JMv)K1!~3sr|C2J19|-vOJ)VjHhVp>_-UP@8eMTHGAAs-gO@L4A ze8v$VFW=u81A!o(XL|raAYRzN*XoJcAfA7Z@Sm{xc>iWL015#-+k_AFpUnQ>+CO0m zc-|F!JpaQl*nhPi01O0!|0W3#0(}NQ_=#Z8GKTQ+{T(2f2l^aU2=MQghdq(=sRVzc z00BIMAN0@hw;vD;dJZd??^z-MFyG&MJR!&nrumO1{GV0<@PHuCN%#cAvjv}+^xOu0 zt|4IlXZ!&1{!2T;{!{q?Ko9`>EISY{@b9RBPjd0x2IhHggFM#;5QP740>hpf=h?<j zDDeLs3=cmT`ge_iApU1<_axw;zk>ns^8Q^;9smHs_oNm7f&c$#0Eh?jjIB>)f;_7+ z7{LGcCcvjhU;fVSNz3^D)_^Ca{}(^le+(V~FE0@EcRfK*Fg#N;5I_Gj6u`XC+7k%o z1^>M<kca0PS$Sc+z-NTx<>PsJ_~#$J`d?xK!9d8f?7+ZhQVryJnvH*5`?TJ30t0vf z|0MSh{{IXAKT`A8#ZUJs|Bvjze~;fMX@&l`rvJ}+5dP=z1Hq7g<<WokAMmMV|Ard$ zB!zzm0|N1Z{#M7Q$EU!5+ny@&OnksVUhv=Rfq^i7=-)(o8bi-W_%!SOVe7w@1PtYS zrU4Kr@Yw|91A(8Fgzrfl|AW*|`Tq}GPs8ci#DYGJ%D;&OeUgR0YYYYRJX1X=1j74w z=Ro=S|808ygFnyH-!u4u5XiG(0_1xh43M9n_wQgp06yT~L4$aohQz-k$n!K$;d!9R zg|%?PCJ+#xjKmX(_#jX|08~Z_EGf+klH!-)<>dv5KPiBS(EqQ85xR&7`dc?MS2s^r VD{J(pyUC~Nht9|-ts;Z|{{hIE`Un63 delta 17510 zcma*NWmsKNk~JJWxC99#Sa82w!vX|%cMtCFdI=t!;O_435`q)l-5r7kLV)nm?{xP} zlX;$R&L1vyYwudSR@JJ*;k2J1ckd%tt-`@V`sFU+iAs<xe5NmRlgYvax@j>7{Tq#N zmV>cqb42hcS#~kKW!HpX;aRci)ndiX{X&u)><J&tf;O3^H>ll*fAE7pYil`^`m&~L z$>A%R%Ii^Npp5ekcA7(M72X8}{W|WxrVC096OSO)itmaXMVa7f^_CeUY?G+=fVIMe zTEz<A5BcY4<c@#k&+X5Ov$vA6MiFMVNk7++zGbeJo6WkJ(2W(#Msx)xE3hN_kz~K- z?Tcvh7cuo|^%vKTe=TlYo^=+g-XzdVt)XnGfqXUg9geqbT#kM8bhh}F3kI=DWkuTv zw+s$~&?@49zWL-N_rkZl)|h~(zT8$=RG375o;U_V>SbqUI)ABCGQXI7xL&P7{?8i3 zA)z>{wU8MpXLKb`QZ!W3^cYn<tyif<DuUO(+dE4{8gA*}-H`htG2xo)fVfSNYRK%1 z+-om!k+gg0X}5do_O;jvE(X!i8`_=n_r`Rfq*cH>4eVp1B3z8G`$ho)%3jj2Q=Eg) z?y2iaYGHBVdzawqdCy9zaqK>Vt~W?Sv9bWyEHS2`u;V3mxZPZi9e&1-MXie?V_#$? zUcD~z8!1MdVjyAt_Td)akAbHvtvo323#<O1x~Zt~y?<@pRJ9v_k`Y59u3ES**1h<$ z{!2D@v{z_ALD+|3EVPw#LFQ&Wn9+7E^<xTVk-6MvweHs*9ed-gt{~1DY<ua<z&#n= zbZ{6v!$%$cmr7==m42m!<ThN!$?IW)Al|`;jF6_U#nV4B<|ztFN!JK9NR=z|t1fQ+ z=BZkyiUfphZ@%rhe<poc`be;GG{TQxT*f*SU}oW`;op}ph|Qk%GkQn#5%%EcjUt7W zg(1$gnUu?(i6;m%%GWprzL%*(9hi7&hzyEs@U5q4^}j#XecwqX&&5nph4X$Hjgc*k zVn}%{vIxqZ_>wA>cQ#@)S#iq?=lUA?2%U)Vx@QrWK+}J7-Vx`P&v2Mll?;~yGe~!P zPPel5>J*#uT`++`?@mP55KO3`JmU1_#qcN>Gq7qXzAY;F=pDZ3Ly9}iP0wDw+vEFJ zjpcV$6ww}@<T_LD-^CR`4SPFL8JYf!m<_4ckmR~1AnM~3;e15Y5^k%Z@~ib>N0Rt% zf{_pyE?|j{Of$>MZBm4go;^VR8u6-#J<sV~w(^nr^rt}k{<m5A)EBS^0gJFYY;(J$ zD2JpE3bc1;Xw9Fugc3Lm23iPDcSt_R3nAbb7NwOx9CoH{#L;jL-zXMiW|;nVB?Vwv zsYa;wXtsWSt?cY}k(tu3BR0X0S`%y-OG}%t$b4=S!Y&~s*<ATr8MpeuP~(k-SW>R5 z#Ih{y4`J&72$gWB$to0vxHH6Br3c=$hunIGUMOWH5Vj3Vp5w^UkZ2l^Dsvad0#RtE z7umW?PzFP~PFWhmM~);a+v~h$G-_XfndY2VXtdtB2_+;^Hx+#zzcW&3MTt=XiD1yp zKjMcmm30dH#plQ;ohMnPieKf5dj~J>&vOfyZ_;<jr;7%8^bWzM&Hkvj;#=ToZGI&& zGi;48?_z9Vv7~LQh*O+R;hsdNz;5;KzOsyY=Mv{jN&~RojO@;Q(Zj6rdG57T>6~Eu zSncvG3m))vvcSg4d;csBS?hB!F`rrw6nLHL`vHVyX&9zVIC-~7Xh8m@WjZMC*I>0a ztxiyUk0Sa5YP~wFk1I|$m>#Khcww}MGN9f;MzHo9u<)yNc4R5AA72ocM?zJ-3xCT? ziz-B>Qp`_xg;Hbi=QcK_;@zc@)EArX>l5u4<dOaNWH&65;Th`hEGwKO+qP+^l<3M> z?H8#oS&wk5AbJO5)bI`!hqpb&h%$>|!|>&3oS)u>F)&KO3TEex^VwBx1M{RlRc(b} ztP%c6YwJg2axJ0pE<kEXsmd@|7r^;w{f1oWS1xG<-0P~Fw_9&6<D|IH%TW>-kHHVD z)sy>Foh23Bw(*zb<rM}C;|6QCnK%oQ59Nw7ih}p<P<b?c^EnZmXcqzzk;<E2K6F_D z?!zR9nbz@*FitdhJOtjLuVo3#<l8HyuVu>oN<#7sWxjo|@d)EqCWJmz5LnxO#pn=C znD*87W{GyA#JkCN8;cD5ogZ_<ASYUi9Pak+mkNcJ#0TkJ#puDZk7u)9AMH|Q?iOrL z;ad6C-dwxQ#bh7i)N;}b7Y3HOxLK&hiqy`KnxIOT%)(l}LhDQ89$XlR`gw~}h3vn+ zkVom?I@iHn%iATQ3H%zjP-8^|UySX@gszl%rd@>>ot~<pt;tbKPRKsd4@kQd2+cPX zfRXrqMs9ZKnagEvW;;%AqI@Vu_^gXNftV+@6eUeZPoQ(Xz}Zxnw55EPJH=VXD0Z|k zPD&7d_W>sN=frLp=wVDa@=1T($xzxnnz^xLL0l8c<$y@PmD}SiklSZr#RzGgVGKI( z)#uKtD7iLRmP&qPFMlguUhFX+Z}8EF?}|_-@w0H9iio>f5YUCh=Pc1Vx7#o}T2`f9 z_{}kuTZ*LcyZ!O@#}AbU0~`x|O-LfLJTVYs*?Sn3CVIU;aiw)g-@}!M=K=bRRl^)O zV#%?>V`X?lYK4KhFR}j8VACn{mKp<-cdppHvikc}mP?MJOmM;34NYbUVtDrwuTt1o z%FD5X;|a@XssyjmJi!{U#QPt!qO7Wh)mB^Ea9e5g$xyqqUo`n^WkEayRA%u0y9wN1 zjJ9DHTz7->z)`;(YlGp}RH_8BJLh0;g9z^Fl~7TItobSWAS&{L`|EVVV_4SK-N!)@ zx0)e@a<U;K&eI6g$OX*?)tMZo@7ysHr)Lsu{h5cW#KikV{j1CtYz9Id(Cigodb1KK z4TwbRP&uT$2~&9^^;PkFjR8W0oHf9|dK?xOY4~E}hV9b9SdlkGJyE`|XBRQJNciVA zF6IxqW*;ghLv7IZdv^N)vjf?5hArek??THhHgxi=qviHn4Z5uMQT+PaQy%xDIz|Yy z@dPK?xxN%p*r~yL-p8>}*W64Bc*~oNpyQ!l#NJM->ynP6H7tUCIuy3(ewJbkcYoMS z3`rDRVbw!OI&mnI3!l6Eq-?@_8ncf2kGv)t067wLd@(I)HP8J0qizQ0SF6^9FPtp; zS$?VB{`uIBW{q7(mQLMl@q1=)*Yf-=e)<;~(krz%uKI$U09z0ZaKTLs`&Idv+JGb` z!&;*7QF(5znda83Uo%t~!4bgSErxrT(5pYz-ASjM+h3q{=rwlnA$l&RH3S1>7YP+z z>Ijy}R7&pg^{-_!;FS^Jvb4UiLY%FpbnMejl~h($QS4<bKWJdXCY=3;E>3&w{gTcd zt^J(7Xl3A|hzVi1%VjAk>EoZR!}P?ne$Tvh<2$x0Nf}T`8J46$`X%3gkP8lhNf!d8 z9D&s3hvx-Hwj6&dL_clGpy9RHWJu<~ofalFFsmC$(K)8S1!#v#ZqK`zhMaw^t3~Ws z@BO(*W$tN{j91^ml;}ffuj2Nd1dmsTA*p7dvglB5CQE%r>*b~Mr?vXNq!M4b+K&B> zt&4)MIpi&)rRC0M;wj_r4!nwSVG{dJB@wwazP?;nqrGc;Hqzly^jVHYmixO%1C*-H z;3Wh{6$m7B&<4QRHxgWmcph$HT;N}UI@6wzi9p}b@N%gH7;U&%jXz~RGL^iIuTfeW zycPJ(iv<2M{+sQs(otHD^#s#${P}e2cMe1`+)bx29KQ+U_E5t4SIv*(Fp?><hUHI^ zVE0;pp3d~V!`Zk%ZliQXW0T=Pdq|UAG0{xZ!28Mzv?!imCjEs8BdAsCo(8_6L>hPn zDg0AOQ1X!XscP>lltD~C^~%~DD3vUZZB+A`h8TYG9ZXCof_r<v-`}8wDBHF$?)DV1 zAC$O9OG}ZpB1(QCQ1!CBf}tY+9+%3p@m)Ve2&oQW*Jm#wIl{V+uE|NqiYKgh(}=Zd z%z6+Gnx~zgC}d>brO;+gRm7yvGK6oLexoFlEE_{Hp<_QqYC(#gh<NG^w>kF~r>4W{ z5YxKkPJ}tZf|Rw>hL!%x#kFbd$op)jxV$X2G$aLk1|S~<1zl(o!<s5ZXedh$TF$jm zmv_WjK*el>X-VH4<&ildrR5DHulm(>26^t~%3_Y@j@Gl-Uld)P4`E9O|E5xIYqI~{ z8Y>s7WK_AiU;dkepMRDa2?7Wxnlo8A=t;|Sy(_pVZ2S6ghqFZqI-r^D_|kzHHT(~S z(CE>HL-@CXr4PIGrSIBpY;Nmv`BFH4H7!h0DunC*9!5xB?Rd|BNB8HB|3R#8Gu8}? z6po`d2n$C7rWHjkrs{Lr`2zc=I#PwxGFw>mM;iYsjLFU2&msd;psA_V4D-suIo<oC zTiN9cVO1j)=h4?VHD#YeBg5}Edu~Trat@<-*ay?I9)~(zPi;Hy)$(0#$ZdOm{Mn7- z06sXY{b}~>ygOkLMQp59x>^ldIax}*FItu$pew&0g^BQs7`ir|+Wzro!xsCbyHoZU zwN!atHk)J}`cBeA^;TjXx4P9k;wwLC<m~<+L-XU(w+V?SIe+wlaprIcn_f4XrAS!T zK0a*N#fi!e{eH-t2zLRp9zX6z>rDy0Pq<nCJottg&@TIPzN4l6b|qrk9?#|GG9t<E zvuw`_KWtUpax37oc30=(@hU<CZftG&-udp5ioQlK(Q<(CgV7ls(N$i+XtxK&hp%Y4 z-~S-gr{hqTR6KHhf+`4#w>`E_t3qEk!rs4)@4BLO5%Q7fex>;PAr%}JEjZ82#>6R! zpfA|utY?POW7Hl<J#=QHV4}#4*59DeI>;To!U>byqa(T@zjVM~)deI|_?IT(%hO3S z_WAyxd(Vjq9{FQ^s48m)3ScbEni0)w1d|A!y$j#HR(i=D1ijVIX!AbfKCF{v?(P}K z|7?Owa=E<rL1)D%i+>cUi2X{8$Bt$(od`E9YMeZLI#$8@`_{<P8{Xb%WnAti>qyt} zVMmy7gGpZMq90A(3K{pI!R$zxYxjEn9XWP%N*rZSTVl5q9i}<K@AgT_C?lAYy#vYi z7Z*PxD?-KwHMF+=U|F^=zn5MjA3Yq!@}9Uz6c5_WP3M^8em>du3UR1=uufG`t`abM zleIT4bR32k?Ptkr^yZ4%KWbjG`Htif2FryRzl{CzTKL}e>U9rS46pAvJ9#S2IP<S? z39Hnfk)8edxX$qEgeNYSZ_3h~x)9cYfxn;D@iR%+g=WBo?weblE9cFe%JNHbaCsCf zfbVp4w9mYpaqs7-@zs@L3uf@H>G=r>WMV&T)~1!^jhXlXH$lxgJc1??&2r>jhr%$A z7i6Ev?C?fuH{6oppzxaX61rH(dGxoLlUQ2%&hwAa$B_i1LnWU+AN7t~pqKVVoTnyJ zP#I4~CvsLRfw$^C81*ZHO)Ny@_L@C2(e+T3;3>(niDwzp$?s62)ll@yR{56;>pzT@ z4*@6O@NX#i7Npu(VjhaBOW{pcYd2t>To`jgs};AmkQ`V|=8>1=rQ<@Ok^1T>HMno_ zT_}ZkdF0}UFs~TIJOp<sB&McEx-X$%T49P_hje_8$F#y3D0T7&YG{dks(=8s+|Akq ziZD*!k4*9mzPCXe*ep8lgl~6uuPX;g^;J<#^R7>mriYhuJ{>%SP|owPL7ZW4WD1nK zLky}^jD&|>kW`GdXqydV-|tyF>3-eks~*|H_R2ee;O7mrVQ3Wje%j8vNl!2eN3&`6 z|HB<suzr#(bD^97XTh?oyD9VF^&NryY6?z(48As8GWN$Y`7ghk=)4B|$GV!V8x#kV zkl$I_UK4M-6hBIchn-hq;oHB186B+l7++}%2a~SHvNiBxqJG-VwRxqo%+HrUn0-Z( zTJqM4`~Hj^7#+P#Q%v&i9JQ}nkyUC)oQP^IGlxL;lZFTm;qV&&eb=g+G#?*)rg*`L z`W~O;BsMUk(lS84&Vpin8av-FLstG=R@W<4cM1p5*_y|x%A$$XypI_kh7)R(NDf}{ zbq&Xn)<Yv@DWvjBOQ?<c6Z)E&UT@%?yq##3C=4bK=knp;9WU;Oz9=p%KWYC!9g>)I z?es)zvDw+jPZEF3MNs4dH)0s(YmH_Ty7!wNlidugz7xJp)z3yTeVq~XvRShGF-OM1 zDAlxs=ImxigFMkoZbiXS1h&0Q-$JyJQ!FE`n1hNSTR1mkI$N>YfAz^4U>75ELH?4R zLQreSY_3)5SJy)NA7N20O{$wUQca(Wd2aIE(Ybm@v%_o<3H!$s=f~cS>$_J;(dgP- zzws)=KQC?2zNd3jx<ouXek+GN{Q9WpQNju^I{TG3^aZ|Mlk-{Br4(!x15U>c;>V}I z!=+D&fiwsGaZpNG5Jff4bS9W)ZJ7`b8P%gq&c<-N?0;nXqR)K^<~ZHmCD*OsQ$stj zFXAKL-F;a0%1AvOh0mG)R;(xIBrR?mJd*9helIjm_D4tCiKNoBl?Uh>TBF@)uY)}@ zTaB5-lPQ*-D80j09t)G$EPHTjv09Gfuu;$&r=};86gP0v`+QNei-}C^I`T$(U&@kZ z*zx7NVCSGbe*5HZ9Sw{11L`qrA8OZQh5*Z6phl@NU2mr*OYDXslAOQ70LH8Z5#3~Z z8yGZi34dPSW{2xSkCYkYq^Ss^U|QmD%cq@m_YXhiYDA!g{emSeg`l_@b*b<LpS2*e zfs^1PM4SXxfQvICXQ+ChD!rONnS0V@Qk)t6j*-{=YHl(F2g7JtLjIv`5I2)z++WC9 zC-15VeBJ4a{Pvry-1o0m2sTtAP8H2u^h8L1b)1R0_w*^2>f6iT#u+jjWIE5vcLo~- z#uQO+@|LU+DZsqpK<g|UtLQZ^=U-E!`mg`i?jGM^*WmYi=lnzI0_sIVC|EU=px3rp zk5NG`g4+gyTj)zes1`JvW1Z}ZZc-hwW&dUh(B=y6IGgMx)CPWl8!V35RRerj)DX73 z)=nuWO$#tLcRAcu&0#akn^>$^#N7=;uSiQvPq3d1M}isPd(YlOnGU~vI-TDpK!@&@ zz{6pxwiJ{%6GrPX2>O2B-Dc(LjGWj`<4>-2WZ)+fQ*$jQ$IF&9o_Nh$=6T3;zvI4Z zxFJ0kTWN2BCwMtYtd{=nU9wT>TM1fXp`D_HaV8Oh@|g}I7T(~iilr_7%bs67`zGlh zSM<iG2_0d<51r9mD#(1WM_b3sRND*9I)&1}PxUpFdnlLI*i88?)hB+fekv)X@|d}K zJA2Nq#j52+?`64B3PorSQ;k;R92uQZyxZ<QGjkv^KM6awP8C%MW>vAm)|_;YzD+ji zXsCB)8Ly%}!f!RG+TY+re6iPG#>;fqiM+g*qZ5Tu-(12Ex4Gvtnr2nmYzU0GL0NY4 zey3b~W0OXo#IfsNdN->H{1g4?d!H>zX;;XF78BAgbTb)$2pJ52A$}@*Ox7Y3Zpz~F z$%lZ;9MG(;3xA4k%$N=rI76~Do-y-IjTDk69bT1k*xTWxKaIl?J7O#vu`Q=RBZ*pG zrZ)^zCZKU2QWnhb|2S9~|Aqo_=D-YUk=$P>%5r38I}J|X7T6H>ZavxT291`t$Guw5 zdyT0CC03hRP56E~J)lFJrBKhF#8p^{VtbNBveY|T=3daJSkuxfh^Zt|PV4XecwD^Q z4e?PFMvgesS6vw+j+sz!aWcJ)p#18>{D2O-2+(|UG>es#ali%Apx5H{J$GUEV};i+ zn$#gk(`uVF$qN21sv9Q0rIZ|jF?+;R!b2Usze50Q1%~8*U3AtU$JW-XRX>~7+d;?` z!3iUdS0-&<+a=AOzedY2<vxm|V}&14`|endqR&045+LQm_iK#2@%Mm5SY{4pXgUro zf1SYcLQ}_h&%8|OAP62(?y81dDPgmr<gXU?R`!<FQCuYxQRI;=ux#{0s?SePl&w4G z^0MY|@w*oZ@TLz7TXV`PPA=|9wpE*s1VyExp`}DJ`|pzB0`EfN<`i_-B_`cu2cu}v zL^!F6QT>CM8BoLk2|u*=JuB??FoCQvbE3f38O>vYKpsf%ZRn<+L+_7dktUrBT{h;E z34g^T0rOMpxE<Tm3J7zQ4dvo%(oV=%@*S%V`Nh~t0qG4;PnUkA?kK6c6n6$Xy5VYh zJpV(}clTd`@w*6?6zD%fN~{iJ;TNo?vR+fgCfpy@IV2|kctCBb3wS#~p(+CpYxbHT zaj=p6wX-4Kh@1`7BP*&n&Rc#Y{drK_gDJk9_0wp3BCjjQvSSdT45N-V*=;p`UbIl2 zZ27!kq2jUG@uZha76x!9@w(xZW&Y9JjF3<%n0i-fez?zmYi430S!r_WWMjhPp6}lQ z^(agm9`YlRrASX^!Ivl~&7)j{g%<V^G;R)$DERP@4d<p7i;@WU@U29O(fi_5Tw67f z$|ZheZ_WO$)9l3+o4IbE+m_%bz+OG0IThHx0Ks}7!M(b2*bS>}#Wo1I4QCG~P5c3b zRe<`=ov-PQ>MVzv=g}-iogocD*@)F^l2}o1^qiDdQDjt1NXyfyR|=poco)Wi^a&@W zSR17`EdzPhZyX(ze5T&Mu^kd?Y4S}D%*9)ivK^vIjHg<7>}+GGq>Mt%c}HYm{Ttpt zXv2(j%kzR{B8hIxuUd9eY4K>;@JxMqWQs9GgevZ%ZL?t|<o5KZeG_+!`>O7XWGX=! zqD4{%PjgMZ-xYyOytl>3FkZPsjQsca<<=iWXENBbmfl>{jOys=1qg^-;`=dHB2Xsp zvz_vvAiIA2HfL+sI%ae!D;PUqwJJGcKy#vnY3govP01D~Te8>V%5us~B<U}AlbXQs zX6h_9ht1*LFZqc6TEl#NzY8+|xYq|_x=DpnJAMWkUbXl=P*$2nJlMv|FF(nPG=WHr z&<=@e+$*^~bp4bI3^l6|QSOri;q(Ni{i6JEqOW;xQENF7H6a>>%N^n~h%&9hbe{^O zF*40s_bws%+k&yXFB7eXsbH?j8cSL8zxte~#LyML@x3DyHo~Xy0uEvwzS2aoC-?s- zy&~(L*zxMZ=Lc#`i3`kK`3hGw9FvjM>N|Qe^*#xdR(yjK9b(~Am0)qUH29z({l_Fa zCS&6}d1EfvNrLtoz!SLVI!8oo(}w{6PI52WV$4NZ0Iz>mp*+o<-&C-h+o`wZr^C)i zyj}J6x%YFQXKUT{QzS`euh2a+JM?iPv{$#uX&0Lp&BA|(hM&Q<5V+uiI<Kwz$qiN) zSkA&mq|f4y@w7@H^oVrt*8bopV7xEe+M<$kBx=O1m9Qg;OaSHlwDVAt+Bjfp%+Ls( zoX|iEwkAx^&(iM6Aexu#i|Ggvb>vPuepekE!ldS-8$V^k7<E>8aDf<@?pI5jYCKvV z3YSWxB(uCzU)Bplw&SlVS<wV5$t>KlnN*O37_>u$s_JCdgsL$7h!r2E)kl0&ZWqH* zJ4BH>SrY&_QXm@40V|sZ`0Pr4Gb4IZoL=7$+-QqeCKMw!R!9c>zXppaqm2-ImicHL z5P(Xa$de(*_{}t;+mjQx#JF4AoKfi*_~f=5)dg(ULU6DHuQuj`#$c+e31L#TFr>8B ze7mfG&1IQ6dFgP`O!>yImC7CAf8ZUtJe&nYKq^c@-CH9s8SS~?`*HS}J};etX>Eg) z-CJqnD0LX6m?D!0wCur)4sUn;G_0wuIZ2`#H_ggO*Tu`?_tdrQzk@UE!ILQz9;aH| z+>;ja<&Ln9v)I_BYs1$sNk2;B=dhlP#wM%`(7z}6iEeVzA|f`5T>IrGa0q>So1TmG zo{@_wNN{H4WwhKo>toy^cE8fki&c<an;@bSqZN2EDiNX=`;K|#NhXB0z0=~u?8)o} zN|VsH5xq~KCb8_OCx1VE%V|P5#z|scE&ZD}BpFthpG(E^5H7rD4k7(xds%m7jn$@> zJUG4qSH7RgU=aB#iJQ5XNsG<hVh|-Qy5VaXbw~IGyg8Sor~V^I<_XTmQ##DK;JIA% zbnf1oziH^(962j-)$u19!>!*;N^T_(qdHs^#mv1N8V<^3cV&tcora4Pp0<lDBIy6V z3?mk!V$>#m2pW=}ej-SPbIMb#MY3h2)#CRceu{uRqvxj1ZB#~ENn(rjIH`YUuN%Mn zmKd43C2SO-F+Xlht!x`U`Bt(*%8DuI-kirz(j?NC-AJiuxoRfz<g5f`_pE#8#YWsb zfzr`@crk9O;U?L98kNg81s>>@Sr6GdOuPrW7ouZdhZU5ItHn9vxjtE~Pjx_{zCh}| z)6IQ1xW}U{0uv%i+|I*=!s3tabSLx0eRkL$kNqOTDp{P@0<{@96Nj=LOzOeElS)I_ zhh{8$nQlnQ=PZj4f=eiR4Z%uf{1)5DEk9dRACdF>TG)(jj2xXDjP<S2o<8B)8d#ul z0Vx0!|M&ogKtZ(ti+L(!WqAo1afMo}NF+FT07WfvR4OjAx}3a-xO{9&mSybqmshd; z8JM+V*)YO?`o?~5T#K!2@`C{Z9DIELjNq1*p5*SP<lNFPhY^5~;3u^U9ZFLYNE<@Z za5DOUpUrAzoJhJj31L~8f*vIBat(UcK(rFUl;-ABajf$6#<B3mxQGH>#Llc(MCov( z-rA>ZKb<o6{!CKL5&z@^U0y{&y}zX0v~`~D-FdHlqY~x)06TMQWB)86A!RxidVj0@ z%U;)Q5@AE{(y@8^)L)1pmof;OJ$I3gm&EHespm@-*$=67cwS_cS<12M^7KrErp8j6 zuO>4hGkI-Smk-VzO-53PI_cSR)zcDE$TQ;@2S*2_;@62<H|GfQK7*)hegz;c;7M%U zCxeEEhchKcm|*S&S)51tg@yfzVKfWpmLN%B=rC|{OOI(Fv8PgcWH=;B^+x(i%|Jj` zznD6gldqV9H<vS$BIK9IZ7LxVK4GG`WMV@85AB!)<(Lj26^Kcz&BpsjMH|uXs~#f* z0`{mR!7|!eoTHGRJ#TuD4M?hE)TOEMKp|=&rXl4$rLZ39O~|IR0cv%ey6Ahc`vi3X zYFwtz=RJs<sLQkl__*uVUKIZPL7mpqm7=$zO1UF`iHKtT@A-Fm9bVn;%#UpOaQp~E zA!Q#n#0uBr`4gr-7GVC0FJ&KAbdeoJ=5rb&5%nD#R4v5#GW#U^tdx(;gERuSfJLHG z)?{0hz!w%bt?BGiLLj&cok!P^MtK{RY*30&Db;IX_PMwRi)Fo``S@q2SX3WnSeLTu zm<&8ka$^ibrK(_aHzw`ji>qYpbq?K+nxcHC$eB{85DED=M*HzXxtM%a%DzQ-S0v?M zw)4J81)70c7QU{$C4KX!w3|F*V=w!345Gcg#>WIRDyhR8kE!uc@oydcQJSwFdlypP z`zVn%Vtc8DKp4e4ph+T#0Q-YK;3H-tJ4yIsVhCT8hJ8ptz~*R(&!G{8*VwhhR{>rr zKX*uPOrsHL04)MEzG>$2%lx!U;OYg&mqaCxSEjZati@SQg|0yj-&~>#n2h5$4`;II z;$;CaE{$2+-1n!yBV7;<9A~!U*h5nyoQ}r{USggLwpB5|SK=hHHa<p1uX<PI-iE>= zJ3HtX>@@r-+eHv97Ogkhh&9qll&PQ8QE-JTwPso%*IpYXu{VB>zQJl<wfQsdjPO{` z%OUO(((4qVafG|%ALJf~$~DNEy+42gZ@^G6tmUXfP<WXx6E;}Pf;RgS8Mi2(;J_nL z!8ia-@drHm46@q!U_;mK{@`@W*CSQG6y0u;?*#1!t_fKhUmQ=h9|(EpCkU-p=e$O> z`?+7VQKOHNFk(9-=|rOv@0P_JT4re*8e2rveS7`%x27_a#WW+(WgrB}WiaY`E6B?; z7#5Y`saGV;QAD(!Acnu`OG|=@I{p@n6>)dJm;##8zT#N5we2e0j>so!ejR$JP7%>D zVR_;ARfvQ5t!NQkdyM{eUN8uCO|UF?*yslWE*_fAsc!oHv2CGaHMlXdm8A?B!Ayf@ zxauPcD5*?FO<wG+Ce^R+t@JedqhOo2q_8&$q9QKq$cJsC*kKc78yuA#ys4fTkJ7ue zblN^YvGB6{aRW1QILYTIq$RN0VOH4hxL5O{9`&oTF$X{=T59=;a--^^rj;6Ot5`-> zubVI_!QR_p-^TQ|ZXBxx>*up1kQFOl6fc%EPL<=lr7Q(WCe+&mgddK`AK8%$JHjlr z_FL{7jyXOFQ+vGR4fJtzJ;@JDZ8XW>8y|{gXa$K;7k?S-ft32*7E|;7Jj6iF9akGC zBIsV6ooy%xs*tamMKH2;ygr=aT7Ip8%;Mv0DN7qIWoff0{Snw|&jV$2$-N|>(?8^E zy{!G7%$#oaC4aD^@t~x9Msdz1ZvkdoiTUHepLd+Xlu}Mj6JEq9Un;bcc>l+c^;#XX zyVR#R#T!#+t2?^Tj(!DBtqt;~2)qjNulXU!6I1^8XImTg-SCF)3~^s(A{je77iv5C zce(^wSsg7d!Z=F&G!FwV0^nz3MZPp^OaGJtP-I^pXf9?)U?{f?hh7Z1l##-uTLUxJ zqWW%JrL?wfN~&1aQjP~|3TFiQiLLlxtvgM$?VmzLVBczR0_Ag}T+iXjPcZly+L+F` z#74zM`I+`bW6SxfV#u0n{TKiyrA1CZ7A8Q5JCe~uC+oSk=y=U!-be!j9M{Ha_Z9#H z9*gnP@Nhw~eCY-GcgQu;8jY~V1!c?g^`&-)v7?Z%3P-Q2pXS+?rfLf0P68C;^BV^h zJlM1jJ&obNErLpP>AZO%zma@ya6O4uf?hiMJ7(q!7-4eWY;>pC1v`m|R;PSnmEFbL zc@zG-j))MUSz%$#vE{^{SIx||wVrHiIdiGj-Gi1xg@6}RDL3BY_S753d*|x}CUKO) zzg=YH24yp&HbhTV;%Bx^ubke<S8wdxSlMX*vdqq1I=+7~V8YXYgS3C(rQWkGM8*u= z6Ui$t{*32UMUcl0c&!Y+`DNG07^}egB1RbU1>c1G<=lvXS@0Wa&uyXW5c1+|<pKmH zE*+Cetu7>&*cD}|RZ~LPIV<;A_G8m9wrQ}$#$b-9hP{M>d4$T5qI~P{Q7A>2w9epQ zQ*|n}4xMbHF7`^E1@DcmhiKp0iqqL}#|IqoRuqS@_&^fk^zSi{CCb3<kfr$G2|t0W z2~@8&mI<kwj$!O5%ziXu-rI5>-|aq!SIuj7awDAeSKe#(!>xNTGfxY((Fr~7j!@&8 z8J<tfM%TaYX<LtQPPok+xUZdae>E*a0iTS8)o4`m^D*kf9nqbE0A&^G$~6s*7u&ms zN_SDNS*V}BIqh4)<k+HZ=f<WiFg0_rj?5;+z3DG0P6xR1n)<{Jvje+BjHL)mF-77Q zivR{PL!{$&(|HOo3uOZxVo228hYk%r)P<Y_1PP8RBDoK8xpa?h8$;+zuDhp0PtuOJ zc>mF%DYAWKtqNt}$86iq&0A{I!Rs<7ie9dAj<$8{HeUq0uinO91PVb%tkEY5#{2tk zllr&s#fdNUE?j<8Z;Up<!b9y+vWV5+=96dX*b@@j;7e)3k~HIoib|*DH<Jg`e6<j_ zF}})0kcaIO1d=<i{vfUXea~}m=jE1Dg;$c@(o!=d4@XjyC$WLq0KFkwn!QB3;iTIv zu#@}FSG)cOypwyn47Dy-H3byaPx~Q8qBu~f;gj*WcHPX4HtvtF7k4O)quyB@q7TlW zx(dHJdq~5Dfu%=pd@(ph({lZGHxWfXA~riEad>h4=siQC{pkA+$G($L+#a~@cs>Im zj<9K&_-OdSzLGc!V`($aoS^xVSW(R|uGlI({f93rNEUnF<a%`s8_8_HzN{MsuE@CD zgeV1{?{z<#%|irWP(wO-0128{4^0Dr$sSWvfnE^UqJe_Q_98CY(mH9Hq??5y)^h5N z7b}4{2t8{M?|@2GJ!rFLC2HB{&e-ZZM<Cr8qE?GgR|jN#<>7$zQGr>P*~veMy~s&< zb+%>*j~>olC|-=D=xpc3?Zvg}kdsOIH~pGL>AIUU;#sWLucfF(o~7EH!ZnJ!w31Aw zV-cP(Z;5M7FGgI!6WZ8eQKXhdEuOP-E)|yBjG6*T=_4Z3ajJ6Fc9n9V83cnxqd_|b zVTYnNekSy&gxOdfB|gjG?7;JfBd$Q>4>Ej}DU~2Jj6hWs$W3-u(uGPIP_kivjgIH= zc=+fM$s-s`Bp=ihu=a}EGgXj0MWQtIr>G>X_t?nLr6<~Y^md}ltPmxl0!WY4CvR-j zr0~shvni)aZN<olrs;P-;!X*@;Vimu1d$;D!58sTfFvYFVB0icTe%v|BSPW?WsR4z zH&APnSrechKLGY(s%Yr8vim56eECw7_;tA;zsJ`x9xqJy>x&6SWd@9H%&GGgwWV^H zX?Di@IQw--<k-U=nAQGp0V(qlUXiVY@6fI`JLs}*gl##h07hz`N>zTl$*}BL^~$m` zMe3)gZ7{l!*<rto&uW+6I1g+i_?9!>_91$d;OZ2yHKwbk^^Z=f*7lhPiHkqd(GZi= zEK_ZEXdHO3-P7-ncW@($OQ_la-UU6(nmCtvgN#=1?vntUx5U{6fF)Ix-I6Ng%1ts6 zN($v^$^L{fusoS_KN(IMEQytN$lF@^`LGG+!`6a0Gr{KJGOT3>TkiU@LT@YB@!M8l z*@#i#A})V_@t6EUBi;qiNjrm=RTZ1fbgxD$J6x^@a1&!qB8(lkdCto!)IPt0WxQb6 zu0o1*3AV&ueN95J+C8bQu{fG>F*YtVx5_{FL1IEQyFpx0n~^2<<jansu}b<rFNyG$ z=31Us)X$$}h!=_vUg=m&Qc*mv4;_Cd$_KauJsvx?yI$HU1y>%4g)38^AH0o-_~F5{ z^U(enyI=A2R?4xbM(P4C_sYVdEeyl`&iB~ybM5NDx*H9XdA)G(&s#?(wV9x0wb@6v z9gE{5G3;*Qi<3Hkw#xYyOHbO2j+|8T-!uJf*keC8+>1=j>c-Vp=oy%q8RKTvz$l9d zC)3><ud{hVE?Z}Q+~q6Vwl6KM63hGq$|UPbl!m$385xJx6w#s#4Opiyh{5c=l}I1e zGOa{Lhh%OJYiCeKw^lLZgMv)zHwbPSOIn7=@i1A4QZVZo(<jtf3L7d|xNEA7iA_#$ zS%cnui^$}!dKh8+4MX!#E-d+&VRqd{EXTI@%LiP&u=stEezv;?cX+(&msM4(lE(wL zY-pi=xr%LVja7RpH*~&nHyw5ea?4K+_@*8}tBdQZIy3d<L%gwU)^x&-axxm}CIv<` z?EXwHbM<{@cf`=l@CPYkfgP6`lPDx?Mp%G+($PjBQBWuDY=efCP3^ZjA|94o<IX?5 zjNUCBA<#q2i-EuqlHg$@TYy5j89VD3s)+(3wZ*T1EW~ip2q%IY$u!tR);Eig_XI`G zHM62`obg7MrvmVNm)Xn^+BJs<BBXmh3cA%O_4w0Eg=utunp!mRQ+>-U(12-MXx%p( zGQ2J^=Bq|$y6x^u5*ljRr7XOcI%8tigKAq37G`;qe%C`vV7;~ja{XgGF$>{bh7KL> zi%B#j$nJJB>NA*q7^8<_ItXol?mAqpdv#JC!Ru496MZzjM(loTF!=Niri7*T3Yk>b zq`21mdC|19>(KSf3V9_lv8>zuu8j`EkKcZ#gxesHLF#C!UdsfPhcl9HQ!(LOCqJBg zY3D&}DAg0s>mfccCsr|H_E6d&$0OS&?Mn?jDs-i$sjlRBYpikz8zAL<{~dtlkIX1y ziET{2u(Ww}EiZGoZ2E`NC9kx)cw0cs8)RAUaWH>M9)eZ!^t#kaFkNp7yfc|jSIiFj z&mBhgec_m~AS)J9my$o=pvCGnZ4O@p95%^6i^{U{9iLR=_X!@UZ&zQT;F2SY4Zz%$ zE`p?o)cc(X!9=H{uzJF8R`WG&f;n%bt=G=KEhg#I{@$DI>kGQGq_WssosZD{6B(TF z`<6bLK$mefGeb#NTYjHu@u;GfGc9hR#{ga;0iwz_q#GYA#DuR7!1(-a{P6b~wi)wv zrpvEL*CQT2O@0cD1n}NoV%+u~M<SyC$cO-A!!)_9Q}dyG##_Cv{Fc6eJ{`|!5)O+B zHWRBb7TO?+KSb|1rO|7bhkDcg`5+^)&=jsI(a;Po9tHwH{>LMWKow7A<rxzGZ(R#o zR5E?dlJi`=6)sFN)3fE@6(_9X$0)v|FbsV|u|p0bHi?FNo0N>O_lE4-n@{e5b&QuU zLw^l`AuQvbYzfFK7_IJV=u%Th<@MM{O$j&B%B3^>t|t#;3wLF<j~%CX-kq6#Xjrfu ze6-$xB!Y?3y^*MJ46pYLqKKbCaTM01M{mP0KgrVsAUBRC+0leECkYDDJ)XTJ$dkV} z-v!EOw&*72d3)8<vP%r}l9fv=^*wAv=g`NCwr*mk`z&1_=Q+13PML^}rgr+~%qp-? zPfhC;sax<8h_K{B6_|?Lr?sXnEHGg|0gynnT;*wHi<0n2L1kPT#z{XDWCG;RLoMqE zU+;tpf|LW7vorJLvV#=}T0XhTCY^n#Hei7qeA+Z2R9VNR;`O8a&M&+eR9GAt!)s9Y z+x{|bPe4)sa|bKKpc9_QB^~gS0%q)b;=ngW&Rp)kB}6_!4`GL*K*^V7UqfwS!Po{f zcE-82WehneEjM*}&em*UpIj+L)syiHWn@NW{SqnuTy~fC&d5_K8xs2#2iM&7HY4}K zP~!O5B}X7x4GlS*s@%R`A{xwssN8+(h%N%Xx)@R}Y!beI0BB43bzG<>D9<xxza0v2 z=z<4opi4*lJCD9qvuq!pX`gC`S$Z2xs#1L;n*Z*nK{0d?ONO}PP1z~N_tFX}**>Dj zBd*=Bvbfo0dSUdm3XQO;=H`upAY*5$#LmE-4>z{7AlCZG!HzdGLwh9O`~ESLTHZW? z%!q_MQ@-Icil23r4G#Q50B@{6lvh?Za`a*LR^4RW{zgI49$9(a4E}nuFk!D28G93D zubmXdwrf}C@&-^gR#k4##>YVeM67IhM!P6-ERfIOa5l184F~*>gDM+CLtHDidHmcx zX@*(lkbqm$t<GiMk7NPEcEgUYzZ~?&Zg-=6r9X{PmuMJBS?!2mb<G$@N+wLd6N~w# zXtrdzLp(xQy1+O`<+aref$3DjCCp06NmNRenvkVHuDI_ct_CV_o8Z+_J=y+DzD*|G zU?sk{5Snk7^1ycg&MWhiE170htuvmo*c6DI_j_+nkr1<4kac_0y?-tWgX5tz^I(b! zupslX`#cbRPWY7c{U8pTJAAS1uY9@z3+hI{2S4EO1P^HtKv3r$DlD;}I0ze&UOqUo z>9)QMKbT@BV={WR<)_suDklO_%XNDFSf=d!Ax<Z*eM(Jkne-frxQBslh(%JVNV;`z zs)qTin)ZyQdlm5@Qk7lou=I6!x&+v<*j4~XtBj9*0aMv2sODrc+BD^GJIbJHamjJo z8UIYIf6Yg%;+omK87Arx4#_Ry5CyV!nKwCoT+^^BR4Hhh9MuV?iu}<3wMN%Vq!ZP? z;nxa7LPr9LC+0LDKt$fKGLXdUG7wu&w;6DtGMc>g6Uv>c6^@yVArY;7xFGKAaGMZ6 z91E>WZ#mzoj?paW$kQ!i>)jGzu>0(|oc9iZmuIhj@J8!m38uW<8MaJQAF;ZXejcpI z`hhdq?T9Q{`V3xB!fmVMyBjG}bSY)tMn~2z$I@o=cKFI?4b&>qFKx*>35(q%W?e>< ze%#quhiCnXQF;^ty5^Hog!K5#;rBjOQC}KbdMfWjY3-9!9CK>d#cd*gWGwOSjW5>- zK0U?;M7f=0;KORaHU(-CVQN%0GPa^E85?2#T>omLl&jm>pSR@puKgz1rd!*}_@xMm z*6$lko!a2Ld~qxYdWLo@A%<ryOJ7{kRerGo>RMhT?J9jmmC6Sio0Ga$Vpx_|a3S(b z&awP6n80_0p-l0Ll(#vh!^0(~?U(If1+<6Kyy!E(SC_EPg|E<5EoK&9sRO371BDwE zPjd<4xD5x(W|p;t3{(9&txZJ(N>rC-kT>e-CBhkd1J8_*m`&93*&laziW~1&2#a<- zQmnTpKssY*P7t?@b1BETFV^%#ADtGW<p=T<pDC0|{&?Bx1TvG)6tTZsB?YlxWZOX$ zb*N&|@(*C9nW6G4KoTUw9;<_blwb0e&Lcj%j=zsGnI~&oe+jn-t=z6I1s+iXY+`MZ z>duJq{<ME(>8yO6R6ue<HrIooyOgkIZs5mHWWV@DR@Lie?-yxj?#$9)=CqkCb6Z!B z_8R$CN3Y^=i@G9l`p{pHtNFM7f{`W1FR7;ku<9;gz}!W72joiqtG5#8rjuzER}?&= z!}V&TyyPEVZ77Cg7q-Ro%N4%5^}hG)M2Ov;qhzg>PS}k%t2(+qkvp6%H_Y>@i)E5D zyuSC6d+fZs!tlhF!g#qDc>OlBf}_F*z3h{U#DZn@2QB2eUuyv~RlDtJW*e(l=T3RO z8hLV~Fw<l$iJX*a7tlZ{y=W&Z<)^)Jhg3Uu#_D*2L_uD+R*STe;Olm5I=iUb&7eA~ za@8&N2I#bkvKnYB=c8Q&@8OqLAGZ)?%t1k6hrSFosfh(YqoBR2t0cKa;RH}U__GZo zC2bQaP8{*u1xAs<-iC8O7QviT{#R$+j0@;@unhxu*ulm{?nwF%1f2|<E+f%Tae!c* z(2oqA^bae?q=V*5FSN`V>RP_E$)B;11?%5L$i&2MBFC?V@)vPAVR$e`a-Vx+OG?+# z?j{{a)2ZFt`ov*#`JtYP%DT{;D{a$P0QYv^u((UVZ_NIPa8L3>sao%v%U<|4eqXWm zH%u;r4DtT-6&q^`@z0AA<Kvn@jh3?SW#8>|g6gZHgWK$?7OcArV{)_xb8vWdUaPfm zk%7AiERAZ_#WVRHz7~V%*s#4g5cv)8uFI@A#+coV6AHMGvf>ZStZd9joh^nm7DT=( z-lM<#_NRJqwQ7}Td*#S>=+fzif7A3Zp#$c)s^rUdMbqA*+G-Xb1JQKaSy25xg>?Io zwTQmLz;a)+C^jCyRMgg`t;s20LXofCq5O1<)QVu`hkZliL7F+UoGJd(+X{sI&bBA6 z0WFs_sLj>;9!5yHEqBiSx0h@0xqln2ZPJWcrxsRD+*(N^tsFYkHyE{Yb-YB(NH-$4 z3sb-hU|QJA&sYE8O6zlm15(ha<#d7<dB9#hF4k>~bAZbQQA70&A;w?>6BYvqJCuc; z-Pni)@N}_2I5{~@I1Qi>5En2}s{pR~|K`bA2q%mNRAz^8vje%=xe|j4;n@G@?_Uey zLjP|&*%rZx(f(i1(Xl0-7r;^dpLT7eDu$DSX8^K8*n#X^OaOK|0Dz7GjZMbZNLb&= zm|mD02w(>RfWUuxBqo-^1;fBl2*p2=0-&&=K>No}b^s>_JNQ3s0MOGy&gV7&00R9_ z8#@3DWM}_R+tXSwfa@<C6u|Kh8|=RWKRH6V{$9+%`TrdM!;g~-@O(ocfa@8Ur~SCN zo*fPV0zx_d=i#2>1D=dPDCn;ZLH~;l{2z<|Yb}KHFVH|v_Gj68$_zX3`9Yr6C#IIe z5y1W@qW{{I3-}y4n4OdTIY=%JF3__;fTv`Gp9A7zhk%}E2MmBh|49q%U)%$@0055X zfk9jlz|;R*|8f1>kAoA+`P>HLVh29wnF9m`|3wui`?JG6kpSU@LjT&3gA?!^3<L_{ zd>#Y@<bpm=EeOQ^1ouBdgFwK)vhZYsa^gRC1OP!?i2{{yuVByPKUEpvISU{T&|fyl z)AgJg5R?n@96JOAfd0ikl=EK+|8Hg>K*(P~Ku`$R^B@p*@ZX7qvOn)~0QiZ(=Z6D9 zxSn<D6Ek2i@Na}55cGLHfk2?Yz<{2r@p&yiWf1uM#7~(21`UF+bHbi8^K|6rCkBBy z{+100^skZt10jFc?9&AJt4y9c<6od*{}e?42>c|T&%uB}e{~uN4E|dVz>vQ>_lfqu z0zYMe^I2^rj#a}UDg4C~7z%pk_ymxH<2k@5F@9b%PhIiEXkvBEQ*A$IkP8C+yClF| ze+xR83;b7j04LxtRym*Q?pe-&z<=lLziazR8vkl)t|z*lp9cg1K>iX52!Qi>V9-;I z{V#!^mDp2l1EE}8e<=rqo$IgDL4bc}hW!ck^V4wvo(n$!^fX`oB9My{!u7niIe~z` z#2f?xJ)f~pP8|Od?tkksloR~-NQ6A0eg+Wq4_*4F?ccQx26F!0EdO}3=GkH}$J2m* zW`nSEJWK17mIMC=2myirYvBL)5P<=nB=WCrhCn(0>ShQR5d55DC?_ZAd3|s^sm*gg z4lV%u^DI0m-_un3f204uM;aFZ1br?AT<n~G+rSXe^O||mb<TgK^<Rp?#R+`Q`&09Q zxc&_g_Fwl~PhtNTW#@o$JO=~fg#MKU@Y5~Wb3ZT;{Jf~y0UZC)B~A|d=2nS-1~^td z4j@SQ>1$CT07!@v01{vq7JM4o0)j$N4lXDdD#-W#|JOqYjgJq_(MjLI$<4vo1nubt Q^6BmcjfO@<P899`1Gx9ng8%>k diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex index 3f635e815f5..2674239d2d5 100644 --- a/src/plugins/e-acsl/doc/memory_model/article.tex +++ b/src/plugins/e-acsl/doc/memory_model/article.tex @@ -703,6 +703,8 @@ $ptr$ are initialized, 0 otherwise. \hline $BubbleSort$ & 31 & 963s & 873 & 44 & 44 \\ \hline + $MultiplyMatrix$ & 44 & 146s & 9 & 44 & 44 \\ + \hline \end{tabular} \caption{Experimental results} \end{figure}~\\ diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c index d7baaf0e930..bb1d9b389b7 100644 --- a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c +++ b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c @@ -13,10 +13,9 @@ * Thomas Lundqvist at Chalmers. *----------------------------------------------------------------------*/ -#define UPPERLIMIT 10 void -Multiply(int ** A, int ** B, int ** Res) +Multiply(int ** A, int ** B, int ** Res, int n) /* * Multiplies arrays A and B and stores the result in ResultArray. */ @@ -24,29 +23,29 @@ Multiply(int ** A, int ** B, int ** Res) register int Outer, Inner, Index; //@ ghost int old_Outer = -1; - for (Outer = 0; Outer < UPPERLIMIT; Outer++) { + for (Outer = 0; Outer < n; Outer++) { //@ assert old_Outer != Outer; //@ ghost old_Outer = Outer; - //@ assert 0 <= Outer < 10; + //@ assert 0 <= Outer < n; //@ ghost int old_Inner = -1; - for (Inner = 0; Inner < UPPERLIMIT; Inner++) { + for (Inner = 0; Inner < n; Inner++) { //@ assert old_Inner != Inner; //@ ghost old_Inner = Inner; - //@ assert 0 <= Inner < 10; + //@ assert 0 <= Inner < n; Res[Outer][Inner] = 0; //@ assert Res[Outer][Inner] == 0; //@ ghost int old_Index = -1; - for (Index = 0; Index < UPPERLIMIT; Index++) { + for (Index = 0; Index < n; Index++) { //@ assert old_Index != Index; //@ ghost old_Index = Index; - //@ assert 0 <= Index < 10; + //@ assert 0 <= Index < n; //@ ghost int res = Res[Outer][Inner]; Res[Outer][Inner] += A[Outer][Index] * B[Index][Inner]; //@ assert Res[Outer][Inner] == res + A[Outer][Index] * B[Index][Inner]; } - //@ assert Index == 10; + //@ assert Index == n; } - //@ assert Inner == 10; + //@ assert Inner == n; } - //@ assert Outer == 10; + //@ assert Outer == n; } diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl index e95ce39d4d2..7964c5440b7 100644 --- a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl +++ b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl @@ -9,20 +9,32 @@ :- export strategy/2. :- export precondition_of/2. -dom('Multiply',dim(cont('A',_)),[],int([10])). -dom('Multiply',dim(cont('B',_)),[],int([10])). -dom('Multiply',dim(cont('Res',_)),[],int([10])). +dom('Multiply',dim(cont('A',_)),[],int([0..100])). +dom('Multiply',dim(cont('B',_)),[],int([0..100])). +dom('Multiply',dim(cont('Res',_)),[],int([0..100])). dom('Multiply',cont(cont('A',_),_),[],int([-100..100])). dom('Multiply',cont(cont('B',_),_),[],int([-100..100])). dom('Multiply',cont(cont('Res',_),_),[],int([0])). create_input_vals('Multiply',Ins):- - create_input_val(dim('A'),int([10]),Ins), - create_input_val(dim('B'),int([10]),Ins), - create_input_val(dim('Res'),int([10]),Ins), + create_input_val(dim('A'),int([0..100]),Ins), + create_input_val(dim('B'),int([0..100]),Ins), + create_input_val(dim('Res'),int([0..100]),Ins), + create_input_val('n',int([2..10]),Ins), true. -unquantif_preconds('Multiply',[]). -quantif_preconds('Multiply',[]). +unquantif_preconds('Multiply',[ + cond(egal,'n',dim('A'),pre), + cond(egal,'n',dim('B'),pre), + cond(egal,'n',dim('Res'),pre) +]). +quantif_preconds('Multiply',[ + uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)], + egal,'n',dim(cont('A',I))), + uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)], + egal,'n',dim(cont('B',I))), + uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)], + egal,'n',dim(cont('Res',I))) +]). strategy('Multiply',[]). precondition_of(0,0). -- GitLab