From b96e33511b4a26f20475a2555d95ffa5956a0a39 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 15 Jun 2010 15:21:32 +0000
Subject: [PATCH]

---
 lib/z3.jar                        | Bin 25901 -> 0 bytes
 s-f                               |   2 +-
 src/purescala/Analysis.scala      |  36 +++++++++++--
 src/purescala/PrettyPrinter.scala |   1 +
 src/purescala/Trees.scala         |  81 +++++++++++++++++++++---------
 src/purescala/TypeTrees.scala     |  11 +++-
 testcases/IntOperations.scala     |   4 +-
 7 files changed, 103 insertions(+), 32 deletions(-)
 delete mode 100644 lib/z3.jar

diff --git a/lib/z3.jar b/lib/z3.jar
deleted file mode 100644
index 2fd797b68a3ae3d5a17bad12f77b857b7e2b4ef3..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 25901
zcmaI71C(S<7A;&|wr$(4F59-<Wt&~LZQJUyZQHi(diBjW|9dmD{+Z0YE7!W~L}bLt
z9p~=Y=Y*Uj5HK<T`1cz~dyos@UtSOZzyQ+1O8hk9G9q-JqW}Ov0CJLG;D1>F{?knE
zzcxnxw)nq|rTJyVMT8ZVXr)E&q{qjkBxz`8U?gcMC&#Di73k-gwh!!SC8VjvrDvSV
zfFV*&F#54D$W4Kh4=J91k)j=-siGzq9HLUW9+I4y-P+&S|M<s1IyK)FM8ALLuj{XY
zK>lM;4_f~|3!v}2?o4$5-2mcm0|!HWOZ|VC{q2qa><9f{%`}(<ZLA%QT^(r+E%hB7
z64jwR4b7ClCOcZhZS3bBi=@}?|8$%%d0DTXG|b7gdCZx-ris6<N^vrI%xyX|PUK6^
zrk>P=gO~V}l$7L@gpikzx1C+eB*!L)0ER(AKJ&>V3;*M@@A<UpJbORM{CUX6HZsET
zb;lch<++vYy}Nex20+jcr^$C7Uixt#^b;ezoKK?aKC&=Q{XwRYvp%;U1%EM8$)2ha
zroi&Dv=di)IiDie7CoeG!i2IZqL7thQ;WKk_M9xw++93W0j?^3bv`i?86toLHS4-R
z3YTr6IZar(aiYoZeR|uTGAPXqi$dhYniU547qEhaP*wsw8vGBZs{6{K#0~8-<tP<!
zgKnbKMvSd6K1#8|%w};Ecv03$%MwWnZc~@Fb?JkoStQlCHSX{gN9q>t^ESYOJgdQT
zC|{*`4M?Tn;T5b}=$PA<IeC3V*NMo>ekaT@NJZ0zyaGdJ4w0Y?(3XMoqBI$(0`cMv
z&)xKSZx#H?S2ioYum&4iD=UZsZ8T>9ijA!erMgpNl1gHggl8UurnCTaM53aO32Ij+
zWnafw+|wI*{6_6lD)y+Ct%;jcv2)<~l>vVtW|U$xn5<(A?Wh%aSqQ6rF8C@d(&Ik+
zY$E^p36S%c@LD5kPRba4%rk(NkPrC2FMj-iP@K$_Sho6*iH-DREF4}L!1)_=_ihce
z0Y)T`@KWYSWrsBg`~;Y6#A%Vb#)<Lq>A_UuIb;YoMhsq1Pl<HznQ#l5+WL%n4R5wc
zNqt3^rP*J-YbJj3ab$I|V;Yzyrp!>pQXJH);vu9}<IHG}{WAE8VQ1cBtK%8d!hyEs
z!~#3?5<1n4-c&J8+V0ANkmV9uXu3-SvIfP|)T7~&e3-IAfq6UcQ_K$X+z#m}In=+Z
zn013k8SEPSVQIUd<9KY6D&`hAA{9Lq42U>ILHbP%iTTZlFNkI0O(xK_e~p-?){#0V
z%{J_5TNTHE#LeVyEt$$t-b7HwthJuQ3J^P!KKk5eWk$^n%bql3i6D~*-U;fu|Jjco
zVq8(PCz4dX&#?Xz8#c5MX-S=UuCDYnZZBtC#E!NmZ?(U`yu7UV>Iw_F|7YI=d!J?B
z!`JnSE(?Fvipq|oqa#}`ekGI>>y$RIHg;(ztX;N@ptLMK6_jKRUNzQE@X@)9pCN)#
zcpnBXWrE7_ple1(N7fs_0arDCZ3PSPg&=bz-Dm#ve(n^taEl35l`++g1Y=EsX@wN)
z1%bNzz3}FsC6pBZ!2wQjaJ@729bMKt;hmlJ8T7;YL=VmXH*<3GFMl^ra74h4!1jeG
zK3<4|9VPeV*-;vn%v`MQ!hO)97pq~0^td^*1AvgOi`?l>Y|7+3Hu)bNAJ8xAU@vC3
z&g(3ThnF_FeXO^z=i!#8_N-Pp;Z|hGo)*hTSHxX>Sf^;QATnDll~20Do6^QzLTywX
zk?}RX?b$xisV=Jn?;=<%XWZTljhRYyZ)W3+$;;|u`e*L4G?4Ma*E(J`+`*Zp(-1y`
zJ%teXzD%m~soNTu5eV0SZlSF$l4LU3mx0!8S98hR++MJx&U*|jL@`fivv8*FvIVwm
zUoo^VHKeie?9=V5XBd(@O~AJZ++SUlkztaqpmE1z7|wWT!$Xd3TMOLQn7C|Hx6f~Y
zF9p^w!D$EY-dgqjOH9;XV))sMG`#uhw3nhRlAhdsx3a*u92>V&*K(q4{3KrVc#@Zf
zl)Tl+Pjt+~H_J4>p8T>0x+nJv>3}bJv@clFh$={cFLAUloHS+*l7KIDw9jDL^aL^0
z$9}(OffY+`l(nzvS^-!(i=aNG(~Fx29%f;r@pYFVK89{^m%_Io_OV)@yBa9)#!c&N
zPV2sA)<{ApR_0NujhK2P$x56ynufm!0JHeOT_kyxIGPryvnm!E5SQSwq!vRyPvTfT
z5GtvkQq}`h*nus(XUt9;{823V%4(;Mq~?!Fp{cJEfU{;Ue%=~T=C1O=`w&Fmfcp&H
znHwrxkk!`)tRjhR$TRJH>?=f=CmAT`mvTx{04p~wG}xh!udqA5)Bw<u*ZYGXxM}(@
zY&FmTP@ZoGNO0+%@}Mb*{}}<r9iPyO3YfGl*~!H;x0@JrMwnq1$iOl~8N%FFFZzlw
z(qZ1=3Ihj34aCie@W1--U$$pOox*P^LMrCbE<>=~$;Hr!G}Msu5xJhxYBEF{bXS!B
zS>*2qf|7&OdTzS-@kJyBQ6`~4WVy02wGQ81t&N$JtW&Mfc5jPTkPL8f+(FpQ!7kf{
z+r5*tE=z4);B1zM-3(EBa*m$WG<%=m8rBnr080qnBOFHW7Z-_j3Yt|au_p6C#;ss*
z9PKOR1a$ACt%h8PNh&i#!4mGz7kSi6cX2hipi`FECp%ZygB&x8)E-T1<L(b~K@Y=(
zY<bv^8cIy27ZsN=ly=lw+f&%i89Y-9ce)dULo1j93!2$vL7Pp&9e-$IPD$4q4pMN!
zd|l#v#?aC=H+r)wpGGR^6XGlpNafsay;s|08e2v;s|#`)Ei1Zp%*np%Fyl|n3dL&<
z(#Z>H*nLYq6kZod6TXlUz5shUC6c}h$k<nFJ*Agyf`5AGnFpPJWJ~e{Xe$#6C$VX_
zJ^CC%J(e{6kaVsj`w%nyfEUm%x38DU57A86Xx~{h+j7~(HM7aFU2*jM3*HOY3|fPu
zi&vhrxkGL11dwXVS;!!d+QAZzPC)OE`}^y3%cv2{(39_QI8W-G9U8P3)ENvi&=e(Y
zs@wkILQ)Zyuu74)5UL=x?cyQ23?7w9BL8k7{<0rRdikV<mvxd!`)u>rWT+VgAWrGP
zwX0Yo(9rzKht!9hV_DwGqChh*0~V_OSWi961XJ8Oxq;-f>N>5?Rk+T>>pp55poNxP
zr{h8whbA}Yg7!qcD%ortvySo6egipE=XgcALtD7<YolA&mOQWHo%u%`@Fd}8?f7sW
zH6u&zZJAJk&C9F6o}=o6oQR`tjSpJ8W!L;7(#ghc<f2TH7DhYD-D^J~^*B1&*{8@`
zW2WJ`Fg!;K%(G^gWVh#AUKva0#tud^3)Z99L^77^5dZRSELAF^y6HtI^!T+79<U_&
z75u$xP@aV<w&KRpt1C3Zi)-rW=fh~~>Q3SK%kA30AK0X7la5)V{LH%q@owjAi;b`*
zQgblZ;Qehbd!{~C&Gxv$fk`K0Vqt3;0$D9;LphTTD3Ybsr-h{Ri~d_Ndjm%Yb7)Mu
zaO;$Yx7_ptE@7P_oU_AHpW4p~!@9>sfsL9qQa7pq2Is=qS_+(QBet3-EGq1?rtq+K
zjSfezB8ZFDKD`^&;aj=vW0i`OYKwDE%bYfY>%#?G6AST;X_bmRGreMG)2*SmCU`pL
z?qwtI2xWR*12nbxa%YX9M{Sn%{WvQ2Gi3h{gdcAjPZ=7Xk)uO`3M`L6WMZ2Scj5Jm
z(lBsmhJwEt8fn?5kvic`Vb~sfEq_Zm1~+DUht#(#8SkZpiG`zU01U2n>0P<te?FLp
zE2;yrvLb<tJB45&KNdXPEie6<BZ-&t^f2ZEen2x4aU>sArqN}kbFhmZgzzPZgyZsa
zF3ZW;sB4|&SRl_n!hwKVv<jd&(cOA<1Ffr1`BE7FVp4&)+e&#1ja`eT?B?W<p)GtD
z^3K^$1LJMG`dw9hDB1k0yBXaVDlm>ElC7!FVND!vF<&y|#~4GQ7LKb?s_4h!d?G>Y
z)e-j$%Ve+fxj5sS*e}*;_0Tg3FOgRKFx0fB0CEt}U8j8MIjmc^BHROyy*hv-u|mSP
zdWI{InJIbhrts6mKu%Itz@t>ws+EH#`$l7`Ay;~yqmb_UVa19)!$?FrCT&09CGstZ
zpj+;t7y8M=i<g?IEgBRi|2W-K72tU+)dZ&&$d8r0A1zsn+{~2=E-lU0+lS`@ifZcd
zSZb^}!xr{93sAtIsRT7I;X~Bp#F=Pe;db}cYrB60twodJEmcNci)F8E6QYlDW~ZoX
z!tBmxT6&}tX4sc=izqO!;)ugNezc%ab4}rIA|cC`89jeKtT8#kj+L?WFdEt;to5*y
zg!Z{+>6>xM)8LB31aW^_5A=nvhoB=O>tP*mi<b^Q^nz&`v$nW*8n&Xp1!=?hsMgYJ
z>LCfEf}K14RNaTF;AD-_!ri>)AWHm1j55L7F=XYXr_~5X995+WzVUS(f}adLt7NOL
znm2cH*QlPWiESD(+w6x|TWU>ThkAfLD_b~$4LuG%Fcfyz_Kch7yXznmk4(_*FTU{@
zNN|XYtY?V=!re1z{u#AcAK(z~k(b5x8{?q%yvWU>DnypW;G?{PGT56zXR&lX2M=s&
zE%J4)rI+V0ruOT|OQXX}3Taob9ST%835WiicE*jAuHL{h$F($ek#3g2Dew0=P}3zZ
z@mP3}cEI3?E{JvI+irmW?WUa;Jo6^eqTwbA=oRIt2j0>FUwc7b?Bh&4wd5YyuaKFy
zq0v%NXGb0SxkdPkIVH=%KYnjy+N%6yr!2NI=~YYBC)!2sEEk%F9R~;O!KJvm6(>#@
z?qg}2NQ+R&begOM)zwrwmDX&Lt_sXq9Zni-873MV&1G^phsF{i$Zz^VPH*KIXMLJ^
zL%Ijm$~obOwONA;$|RB5Yhf@>Tr=9-$dL_3MG_U%@ePw`wLh@x*BH-|3t|x`9l8^>
z&bB(r-X<`;vlm|v#BFuTOwGe9;YeF6(#yFQV52%{`Xx9TQ#yDi^K>ZM40E08?5IuO
z@abG&lk_&&!MuZf0-bs@4YbIRTm?cHe`J7fC!qFtJCX3zAYrVhYol+)qd-mj?k85x
zT!3V}Ewz_k*uLC@HZR++4kh_W?+pM0?~{b?>1EzJ!xEcgQ+r@t6cU>M-UjhzQj+JK
zrhzRZL6MeSueewX3lJ9Hf6l|)Jh^299v#cbgB#Pkt5hp$D=!ybt3$WMHe8m`S?}{Q
z+i5L#fTUB&s_`z=2sJjCX{IELFRc)e^>9T*^BXBhTl7ZB19K?%&hO#$x0BA7{g^lN
zmnKAbH9-PEv5BXB4Mr0Xqw6$*2$rStE+e`x5(i)U1hnG{x4C8vmo2C5FXqb#DubIS
znGY>94(^|u>=GNz;$*Ew0?lT9R}F|WS1?S8%)$5wD*lBNT=2>L>^pKp7$f4TaxAfr
zFv}P6C_|_dsWr#o4?3TVD*V$w>FD-3X}A7?f3?%|!rrrySFDXmw+%8|yI^fPYf!0<
z*_5VaQgHV-EnS%gO&O^689OCs(N?*a4Vl+-)GL?hE6lvzIQxXa2{$8r?l4QR(J?KC
z8!KEJ0hwXp&~l+s0#}joxg8-dI06*CwcqkRKtDu2XuQ!VpH??nWT}#1-&dwa=dauH
z)g+|fw7b-)Oy(@nSElb!`*FV9fwH4H=eQ8UQP*%Iv)XkTvdv7vwkr&t7>GJE;MH+t
z(9<f^D1XQ~0J(`RK=rJ>@CJ@v`y#4R(KGvw9)d9_NJadgBjO^1j}#}Sjt0Q?9l|ZK
zUfO-HOnD6Vi+npGBx6riH;HbB#oy<(>(aC5h8(n%aNA0VJv3xa+8X5RphvQzIIR0U
z$9yIu-LSKp@P0Y!88Amq6%SKQ!X9G8>mB04k5ff@D#u+h-ab&?Zahn9W9LAv$`Rqv
z#b5P7U2uln;ktSCKYX~1z<FOUUySVs`#N&TdiN^dBEFO+k4!P_3+^AmjkLjz&}HK*
zRB&`j9dB)oinA9Ribg?1#^@4U@gsH>see#*deFH&-rI*9Q3oGM=V`lj+dn(eXyDVu
zputST6bLr?roA&en{5Y^ZmTk1J8zt$w;wh?m`5z;U+E0GIHtSm5;(oVAek)T$~9H)
zwc<Ryyg}LB@FStk_-T8Vz@v4U?HZKpq2Y1Vzwv08K7B-qKW+5eU+Fy!K%I9+XNn&o
z1<t;3BmHa>Gl4rPfGW5fVLEx|&voQ67C1tkZHaWeL>4=mGnswa6FBi)449k~JHjZq
z8wEV^yp;O+TZ254mo4|syx<PA;BNK%=4ZvoLozAVfs=_;6&-RN@YgEvb0mljfG&0a
zz*btbt6~prr&36G7n|M9;r9Sr;L*NJcXw$(+MXo{Xg^o_2i72+Zx#f!-pfP7o6yd8
zEdraLU69bOsFw$prZgbF%mBYGnN)h&CILTekfxt9e!Nc9^L;G=->)$7bqRM``2@{`
z6_vk(H;72m`9PdPah%ZbiqI7Qwj+M^nqc<^ghDmE?D%oTcCR+;1y>Q<Cdd3+Ye3L8
zVzC1S$De8T1uy~I?~PWeBU~*zxb-cooFzf<+&?)K3yucY9uDs3)lmB8Muwp56GOT+
z(IDY0;KMa|UUMiICZE9KDn4*K9seFfm-yc2fjjPMlmjFV9lxyiJ>KL<>DhAj*mbet
z9uCMmTyw2}?q}pfeu)=s)MXM`)ecKAeadhBkLDK^Y}(^w33NYwpi?`8nTCKjgvi5u
zFGetFb`hi~4PadVp-ALE=)6?OSQI}47>KxAdOSzPe&`VE0g}S3VGXjZd%zVDUAX8w
zUy@G+*Z7d%J#E_;)bG(!A6{8y_n`BJC%;Y|FlR1pkHk}|`5E792HvoBLu#CEs>-uM
zi#~Ng5EUAD42Ad4RGAoD&{iCg`HzVQxn@Aizwv`cw88sdtKK9Y(A$D+vD435Jb$@^
zW(APvcA*2Pg<`RSf8qS4YVK(;5q2Q~04!4dEhhf|i-2hVE&_^L+8F3t{;dHTE3C<^
z@xf=_4BD~U0g@KLS4lt~<gvzvy7~|n^yi5wgXbynH|LmVQdbcy57&m9E<~Rymh;>L
zy-FsQMFEK=zSc0cnf#hu$z0L>?fni6fP{)rH^h(qxKCw+j{xax_#2+xKo0A%pASDF
zuiFXiRw$tJs13}X9k~jdut4SF4=o4PvEqu_+MO|3r?b(s3OhvXXQ_M>7Flj{OKdJ^
z8Z5Me`Y=Fo-m$+Z@&M~Wgwbhq865)i2^q8(a03GA>JJh};bW3*AQ$(cyAD${-%3&!
z^e$vPVK02oChuddQJsRG0N6b}qg?QK@YFq_y=4ak)YT{V+;((1gAaz?aB^6Z((*~|
z1g<L=Oi3&?VPWNz(ZIaxiOI(--lm<5DlF1Q`U}+i4-JmWeWiSRhn#H*T#EGi-6Ruc
z^)%_!_E3{ww#}2#Wy4j}n%U+oOdNkan>??pW}Y;HX4d8s4p^*JQWP`}iw_q{-K;K9
zRm~qoEEA*xY3V0M4eA^kF@AIGrYIz0tnZ^VEMsGuJCvq|Z_%BfFP$Gnty{NscG&MY
z->;!PI*Uifs!MmO?Yk&LsXx81C={(S{$emj7A{9nTlp0C4yrGHSwb2AwSxZTsmX4^
zegrA-B7H8p`RCkSF#6}_{Rci`EZXxt#$H#h8NK8+H>>&a9`a!>paV0|DW?}}AlJu_
zI?Bw(VXFOwm8+PKpOD2PMG&Cd^dgTVUV!_2VCWaOayjgz^<Futc$pN9pD+>-FrR|?
zvA9tsD1<<I;sel?*gc93MZt2PP=5iF2m-rS>057y`WCYPpWObR>hymA^IM(%WoGg>
zFe4Q;Ws&%ic}yN>FCYEZ6l%Z&g>yC(Od%0LBE%^K3J&5>!x7z5dKDTQ)>=2xOm~0J
z3K8A(;B7}UW?AuzU-wu#AFfZaZKb}voV~#T4EGTFX_!4_C_0Rpr-AS69SE%PG@XWT
zC~oe9-=?lGYu|!X<cHy-u9_4;CsMDipZzf}au~MI$$Qo3@R)A2Typf>&cBX2!{3&H
zN0vjm76c#=V;C9}g}riYFM;<HSOEJdaWo$)0o4b;EQJS!A(&^`0J^+ZNo4bwH(*gV
zzjonT+jr*Hw8I&zs^0p8PI5X6mfgWI_EUiJ&z<fFFg_#$TsJs@JzWK@z<oA~7Y^KN
zxOBkq#?OAyBh*{5Qt1=rOEp~erHBz(nl<}uf@jTSHf;Ej{$*k*H}HFWVlKw_>li;u
zT%Rzs1ag>e_CvQhE~k1n-1Ii?p@L0?iw+BC1SCdGN%lx71HS^>!Gy$)+Re@9{6TMx
zu^rIS2U}YY2HJX`f|E?`pb>aNBoqR3HB4)<-jbq@fn-@svI8l5F@v2Elt3F~xd=+N
zwc)Ygwc8a_3)ho6^sF0MCKMC`+>!c`!IAaxz~4}Ytp@a7NFX$gqu^p%A!nkwY-1e;
z>N7%RO^oFStiq%d)rpP4kOF`#p;P-_*0t18=UMybATQ_SoT%`T(Qf)_W=Q0e@{=kS
zMeEqgL}AxlhsUqKgc6xW$C&apze4~NpyVZ0ixz(EBD*;DX~}D1w`JtO9cK7}|H%2-
zkZ54xI903njs28!Ws>@zR@4b%n>DNCHkGxaQVW-$OMm86utuJvw?CjaSN_n)^s<Hm
zYB{1L)3iQf<w9vQOFslo=-}J^#57(Yd!~$Xp!mumBUIcOKJLk(b&D?)e)vB6B(r9>
z_|4ptDXdfyUl|AL`4yD%ldlJ}^XX#xgMC!}Kqm{0&3N`VJ;jXW^#YmO(mSL>Z?Q?P
z`iSUMzvA*YbRB>{JeGAPc)<E=v2;8#ryhSV7JlIWwOIbjO?{_?{?7O)JDOQK{Jm1N
z6|7|E<dAue9wXbF>6|Rpfa5qp6@=4vz;r-KwNsJSQw#+J0#X{4W(ymFP?6r12fsO#
zKW{glaXS_!5gP}`5f9xH@zHvASLYXi4=6f#i@v?X1sGi)IiFl~J-x(|!d9dfFoTvX
z7qFM{*0~IR`4<CJeDeqeS<Ck8?$OaA4im#7N(@4R&hM+{wJHabC)}-hJxFp85PM8;
z{6p750_v@+nmL@7Y%MDLJ<0M!V)^aC3AA<^oS@{|^bM`MO~t-iUm$R(-{VU?!Q|IW
zXLJr^2RtKf6Mo3@2{Y@s^u$V8#Xu@nQ8I8_jA$TvkB7f*O<<Hu<bHK!qs%PU9+C?&
zS}qEJjTjWp)CI=dz8Dah#b+>dV<I_#=v#Da#Uidw)9$IKQcFZsVsPrDV(LH*uw9Uq
zW4(Y-a&f~sX(ol%73^h6H4K4N);qWE;;A0}6c%+=S}YX78Q9oyZknSjEf^l>*S57)
zHF(vxnPWS-h@B@@PRFGeVIk<EYOmY0B8^BplLS<E7im&+ZFGCkm`uP-%@VaMA0Li#
zajz?5Z!}Lj>AYIr-+mVpqK~rPrEZ6m>1Dpp>yFwZb{KMyMS%ROmhy!ZIN4%--3*ac
z^Tqh|D7%Iq4CZCmA%%~5wn{VEcRQsjso%o?GR~v8#h2UunV|$M!3E_43Xs_MGa8H{
z;WyA<U|Nk4Cx`k5Q`YzO-y<*Tzk*4FN!rH9_@9g*QQ1lnQx%!VC3)k3HiR%I&p>S+
z+>|9`Khm@{he4qmKS;<tuBvrc12~YxX6`fGTl|ZU$EoOqm~?Ku;bVPkdTaKi1q#!G
zF@A*J<LQ$7i0kMZVNbVDU0q*402r2u@X^jH2OGV|N=|`WM{l&eM5|@kn*NlD@U2!Y
zNqv-xcc**dX4k5ijNUkUu!!f-VZSu=B#B@HZm8!M9chATx*KY*8Bn-SHfy#J*KqoR
zVSzw0-kub+8?u65?}!CqfM7(@G8<fHw)(=tK)6qP54VHA-ungnVYLGb_0LOhK++=E
z8i;XtSLfp3*5&*Fbat#^M1t>4l`7Z|;75<^f$JOA{9TbtfX<_tq@g7%Qg>0kAUIdD
zRMQLfwrXfqRJK6LM72<+GgBt4$n;QHyw-X^$RER}=Oqh=TVuqZk5REOkt5F}C0LF*
z^^j@C84z;?)7Ze*jW+4+L!AbbuOiN9Z%9w;4~PcQ{5d7=M~?_=vMM8wK}av2gJv;m
z#LG;HLBXjH+-U$JV+gedF!1V2+f(SEuG;kYU{xRQq#_d755c~Q@Zv6w7mx2-He5-&
zIYAqlt5auUDNd&4TaHZI$5LQ?i6KoK&)v1L%%NkEm*+m|f)4Y5irF8uX{l@{FbbU$
zMN3ktPygb`%>0(R(PFpR?z7!ss$`zFVvY}B+*ZM=YEEh~0a8?@NuF4bj<`N35qUV<
zllwA`h}6gcv^87<sQzAce6E!9&U>1LbXzmJeu@7P4Hpb-vCIxVWSGm=P$q1U8B5-)
z4Lo>iS3FftbF&gRHH>hlWV@%nVBa>Y)DczYY@otQWwwxX8DO&}&ejE;`Qun)Lf{JS
z_vyW;1S76+LSDx(^|A{f5l(whr{)0ZM26Zbr=MK!A`=o7*;hzE9vML|1U8*q<lcGc
zyZ4xK6y9@*uCmgm7OKmugBjs%gY6%I5LLpmu+2I;e&xWUj07E`EgRBPk?f@`mBK87
z9WjW~4C)fmu%xKV0+UQx#?P^~F^h0w5_p}4NJXpA<z%$+gVdgv#ey7LvxOO6;^qyC
zg%PN|z_G+$<$lffjR`3K0Lb~`YaX2&-Vr!5m*_=HPx1r8ge7<7%id4_a6=F0Sgcgl
z4UjDG-DdvQ5b_X8c~jFsc9~mpi_N$Ef+ZT__blWaM=0yc#I1~cSl;4RWxAz<ER8H&
zsY@A1%4jDc?uMF7LQjaB3xX=VI}F^oFkbPgs6eHo7)=STJE?0eYCc0zd;FHK<5rr2
z5dXTEGi79J_o%7pu-y4+<XZXaqCqJlWR5toG;9c}!1cc6AK6o<RR~~PmUi`{yL<|{
zBGls!cRx;DOoHO)?OYZQRX^r$h;E4>kM1U59IYseYOee0B=;4f61r**pljVdDHvC2
zfY&QmuM;=!9|rt(A<NbgMZ3Ee%Tfn@br{n?vyA@)x#SHJ2j#iARFSeaPQ?MYx!%==
zXYzq$>pY73erX|2-st`iMd$*2CVfWDtM0j>lDXdAC2vHta}-b=Vgb+iV;+qw_+)YY
zVLzGv<B9+G&>JGDVfkhh+wR*YKfc74&((riK|~4wtgSw7Zxzz}uNk_T(cvO>^p6vh
zV|Tbwk*j0Pl;=BcA=dBj(M<lVev?z2acW>4pEK@$)}qbcbxHW&{$~~BlM<+aoKf5=
zvRuztpmekMJ=n9I5I`}0)}8=)7xOUzSOANbxTrCk^inxnfO*=z$JP7;JhU3eW(~BN
zalHNCSw>;9XnhVgC+HS5zSvPoTc*ioxo0TCA-UJ?O1Sh1XTg3_M}j!8Cz+lIit-!O
zRf=r6;OLM?4_iEhRccn-%J&0m+zb<js2jA{0pPk2{P0>jgB$pz!EJd_P&S6q)!pNL
zENt7YP7kNFOCe(lDkn_{vTIn$Dyg#m+ata{wyEcnq||Oyo;B&^7r4KoKdQiqeJcn6
zK>T-o$bXOi|G~Qz-K-33{=W^Oyp;tKKYZ3oN5`0UoMd&WIFW%_XamJ;N|2utjTRv2
z=>rQ(&USE{W2I(%+kGAXX%`}J58Nlf?*w+2KiTg!O!ZS-chq<1SG>HxfAE1}f=|+`
z7Z|>1NE7?Lb#k_6ii{YU@W7H0_`N6$NZ{e4YX(;$6nfi>w@c(0xV5K<Fm{0FTh6|$
zT4j?`E;9b<ru+fc=L@*ZoX1<rA;5w!QnlLodmjWa`vmz1972+RKw3V%a_TnkLN7fQ
zdKp!~P|t=fC9llBTGJJ$T?tw#F$Kbgxj38`+f9)_)-dp1FDyp=Qxx7}7WZmq$J*o1
zWx=~q8W?9xQYuIrFXw*S`iNoZbXCpKzN~GhskWY`scPN~-i-?I!>WrF{px6ug~5`e
zbTpv5Iv(wnkM}_<RCE_PTlsr;*!uTFl|dWso5@#Dq)4ET!u6x_V+hN<8}nv7Xqlw2
zcFqBqErH~<&r~`I9!`OP!56|sb4pS3DpMEUC?p*7#Qui3r)(!wF8pWMu}t>Rsu2{Z
z(;8S7MqK?w@05xOZ@;{pHJ*ixx|WVdpbQ%&2Ksu=2VZoQFqU4%0&o(ac1r*Ba=l5D
z8lhAZdn(5;U=PQnBe{=%Y{sg3TN9^$005}`PfCFDuaw{){F3-@f@!6o{nu8EdyYoi
zS(64N%rg}5PowgRQe<4it&fC2-E4mn>1(4V8M{%N;HtL3JHjUnQnnDDIq?nHbN)PM
z{Xop1_^-)L&ZA9_%Z-<Zw;@>oCw6FO%|U<MEu<eN!?+@Z=+-bEI@=5>)f#lL8_6U=
zes4Rm`5jTe5-_3XCUo!x5H9G^6U~zeKD0XXv0os{Ld}At6crt6Vr%sYBpq+$UK3jD
zbe)jA&xjEj3+CNa1K#m3-#n*pJW0l7(5+UENPnRxA$h<D#~wSFsAk>loUxySJMoUi
z+#RTkUP@rt(iy3hv{$wcZI&JZ>$vVmd_-a&$~Q0sg9I5IK;|Cc-RaDiI45okV}Vf5
z*v6%SG49XLL-w&eg$2i9G@I$8Sj=nQ>p)`^$#me8K3HaV5^eI9GL5&!`L%BHl}rv^
zB$5SBzelg)q(v;CisqsX070gu&RgtOMMBm|h_B{RER|Stz9a|U04%tTc=OS9=K%!K
ztV&Xb=>+n3QWy;z#<7T&B)R>t2v~1nEpgHkl|bTA@ZoRnxV3y>(!YVDA+}KDu7g6}
zEa=)B1Ru+$ucqFc9rYZjr0W+akUdJ9OdcfMA=OVcnuoxPPbm%{Y3<0ICzLvaTvHnY
zJrUo57_fv-a_Z!4xcDtyfmFs?u?oJh%C^qABwdn+;iV6sdD4x1S>FEp$6q0a2g(rX
zFM>(<KezV(h9(UrMH~BnR-I|fOWPnZz-QL(Z5YKfTbe-?;tlgF`wHeWE9KD$tP=0S
z3#>Yt6`<N(lY&OfZv5I)0=y~S_Ure>>y8!}C$-(7&$>zfj=br*UBBOfeSTIDx#}}Y
z2EPVkSOm-(6G<twvEh`}3fN|)E-xQ}w*+U30!dUF2~|ie^|!LMg*m=z2(M&3wa9Zy
zOIbRd`e_2fa=?9S8whVbQV8#~42NZZ29Sop-&c#km-*E$N#`+3=8f!sv)t*6z)g4r
zTwEG3FI)|}n_7JRtgWk8icbjPQJ0?bbg)$zqGar8CMO?U_uuSD-(0klPbj2I7tLSv
zHfzGPB^^IRf^Nr_2(08oW(&Aa_a*8_-8{GA%IrAbFRRPc-3|8A1@Rjb?842w5=EO#
z&Q!I*BvOPS9wKFZk@?{7CMDfF3d>^87BgyFvT0iLI>^y0%elVChnTW#LrGvW&Yd#C
zYUw%^ZI7Y~sqtnFuWXqGVq&?!!;eBLuMjtQl{?^F(^4a0LK|KWj6Wvg*zLuMsS!yc
zS}&Z4t6YISMt0=POH*{l-TH#vR4qeiU&(ysi-63u2rw2ykN~(VgO+qa$+*K<&l_iI
zK?x)5;TgC^w*LAD9t2U1I3~WMi_HIwF8{WB)nMZPF01@U5u)-p9Ok|S$d$^ARa$X2
z-vj^<4zx5v7W;Au8sWrsKKXKT65_A~3G79E%|>EYr$w;QY(FGKFmC`}NCxMfZvAhb
zlD^T@<^A;x0YJcv(5|0mqUcm%0@=g66&jRZIiNI2?Dru+wu((iZI#hDwBLH-0jTWp
zQ~tvfx7?C=&tSZ5<)mHQ$w2AQrydYHiAxPMS!5ingHP=OA<yU{0SgxXnJk`Qn?j&6
zS;2&wNxSBwPzx9JIJZ;Cb-gWfe11SmTKY(rES7W%Szi6dB;RyQ6{}j%lAs>FNoypf
zW9`ZLBWMC=2X?>h!qp&J$TooMikI&tEEnIk`vMY;%y&OSHJ{GnLlg|{R1A7I8CKJ#
zO}{%;&4p}dNSyr&cQM;K)8>c}o*FXGXCa*>^v%uJWC-<lBOM|3MWIRMBg+tNkP5mL
z*LvG5Tcyf%D<O3xP;2&Cc0dJ&8~8+%o58(S<b%LmTRyRPB=b+{V~)fx7Kd$Izh;^Q
z#Ebz|;$R>Pcs~Dqk!IO!i8R#L_&?+xG7MxkHast|n`~j|%fd2V_(F-6{^r61!6-hA
ztw4!!Ad+1E%D3$~ZIVO9bvcTfd>{Xy9#w=^QiI<(5dSwET>nR5E5_eX84V^?dwpA5
zV|!w8YezXp`@g{;EhBBwD+iwuNm|O_tu%!T$z1{l<c>n;E0ELRmp8o@&O?lteH-U`
zt@}XidJT3jD!!DnYwTk3%f;lAwwTF>Ck+<T)=J5$9dW!Pgh@QdM-PSwrI1J<cOw-c
z?9+Kf;(|%xmTE0PK~@-@X-}##RcAQ*7_yAlzXi1|bH3xxG87uBB^Hdp9sM=#sz=VO
zUD?VWPqVLr!dtBvVk-RUk|7<c`GHrkMT?l*-ph|oJzHy^{5<eG)>@1uG?7YdpkGhm
zuM-D|s#IiNJkHHn<oS~u`ip!ZED4|gSSl91RsieY4nY5Q)Bj^<|LG$5zg;9}WA<IF
z`%ll%$n?PW@F8a`oSssS!i8XQoAxSe5yKLSiCtM)8KtjED8hb@@)N`Ibc=?n+PU2w
zPDpLG^G>1pAp8U*#bkwM=Fq^V^|zz62W`}=A(bdM7}a}3^Y_t9x*!p>C~eTnjE)_5
z(NCBawybx+9c!TstshCCHR6%#l|1&zzsP|M*IKImT0&n}c$kyJdv{70Zq6C{;P=5*
zW+=sEAy@p0%omv>J&d)6hrIf6=yX-G?v2Y||Ds4e>TsJB`tt@d<GV%~3>?k?X|VTu
zc30omf1f|%-}C>!5cwM$k*W}$$f_7$Q@_~iSETSQ#qh;))g;(_V_0X*A(Z3c^^&!W
z`(lL#MlOk=IXUac#{qlV7T-DxDGj)Hl|d@RsnG`(%gwnp;Myz6a34C&DZIDRlc9F6
zRK52<j=Z*>I-j(!JZ!E!&Mzqdq$SLt*|wX*o`mcOgWxx@`fyzF;I58Nzzm-82bDa@
zgBY=+cl#pncJ!&kq6cd*@xpf}$$4-G$doc7c9o!uZ$`*3!*atCm3I`mBJSu1+aW&F
z_IKvE)+=|VpiOQtP!t&|dQ1$Tu_p(v-PZg1I=DJi2hc`MPtXjTVRgfH#-1U6Z>R=U
z?^-Z;;yl&w+LSz#V%^iAY^mJ%_{|nvJiS%{(wMCUty!OBnYcpEPa3UtHX1egxgP!a
zh}kqfc@#5Tb&>Wc5at(dGxX@Rert0oH;qY~D6)E$Rg{Y>S*yffzcdPMZJuk0yfpA0
zwtc%N2q!;C$~S3hmEkFz%c7k6IY9ujL{hbWAOTrkCHCe{x>Sf3Ac6v?Af)UmI^d%0
z8Eue*f5^EnUw(F)51B*^${Eed_V}~t0?S%*Lr-GhNj#iopIt=}3ns{#szjXl?C_lI
zWZ$&Z#`Tl0-j=!)KW!@ZsP8ZYzW_PG7{($EQKlduFl*=Ov??pPR-9NNdZ~pmcatsZ
z*_U+{AJr0mdelpG3f*f`CEj1XK4!P|M;%{S;YY<z>)oMD?7YxGyNRnB|DUUf2(>}n
zjX!2i$vbYZ;77a}=z9K?;ei#GSPmN$Q%5DgX7gVNh7{n%3*syf^E_$k_0no<?1(W~
zI->l|hDbOikV=)pV5&xsoL2}1L6)u~ExSoK_`z>EWW@NWp&HS)`j^d)<8tdZ7aj4u
zLdo5kuwueyJ*%dS&qAA&o48&fj~sBo0;6b(j?$fjoMPDg4fu((&zwDdM>=79V#`u`
zV+{pwLB{q?5v;2BAT9sY3%EpQ{Hh0R3rp&Dj4jhPba8TN7;6acIi)$w<r|0ScfoYa
zEv%>Wf&H=Ox6%l!&l;E;x{)0!h$J5nEH3LQ91syAppc@&VDRjS4WrrwYzV?JP;8jv
z7F~`88Pvvl44N0hjCfe{-KEhq1UOpQrgzz=pJL3)7S3?ouHzsD@Bop}SW9xVH)mmQ
zBBU5=+=`8ny^;nXh1ME$_B!iu^r(>erv3qtDD(&nR`Bu)yNN*-ItJE8My(K7-lxco
z7^g6sA#kzLOoR(o3oZ*63R~=19_xz|OOdoher@2WXZhZtQ&qYA>(cbXLd-<nvl|NU
z^tIr-SYPxF5)ALaRLPa;GY76h&G{{%4OJQ{4kx5X87IedyKEobwWR%<j}@-fqAgRi
zq{jNa1gksjf;^ElW{^}{>@Imis!Tp}W-*quNq#n+k+kYSHS;@WmwXPh`7;fz=`#*o
z*N_{`?`}L6uJJkE9YC|RbQP4}i`QuH%00I&Sog>u0yAXgFx*q#pOLR6L0x-z^HMDD
zNMEzpHc`q872!Cdj3Pa3IGTOGuS0^qb_r0T&6|fwxq{M_v}T97gp~!-6!HRCNc`>~
zRVK`rjXhdz-2007Gq)z4nydEAm&f0fCM6!Aap<4<RA}Tf?|}VNWY@%^NG>q4k*PC_
zCY_Y|O=}{-ej+SDt#fJ>*zwc67A-7SX$EB;oRwviaZyxtL>zbC4yKR^s|HCJc>UVk
zR>-94MHyrpt*NN{6FQda1f~5)ek;}4-pqhMR3QqsDKjXry~U3hs=?SBTa-K71NLqC
zY?i^<tCf3+n>NtW?*xQIvWXB!lqG*{KDHU@76s1{w^ayw4X&TEm^-#`nNWjyf!!%O
z4BB{vtu?aG_k4HdqyH`-PI}cDGmCw{a??@e?6a%(?kq1b8|1DDEgDr-4O<+#(e5Y|
z+gUo>20D!_p8u#0yOTqrzfglaKR3BCO&N!1Z=d^TG4;`K%qZX#wYv*7EwH2e?EOuq
z)R+k;mWw*AOCY4v2ud`Pf<uU=!xa6}Zg=lgvi(c1{Yhgk+qwBGP|4fQNOSBp1v3;u
zRPh|!A7M;31Y?+70rb*rAA1RE)7;qXRz8wm)8eZMrrkC<LUy(c{t{jtM&D~<!aZ`F
z;Ga>)QB34#*?iPGJg}8npM&x<Ej*p3h~Xy6L*f*+DCRYg4@L(M&1sD}Dj1fz*aY4Q
z#JCwMD&k>_bGn|P^XwBLlAtrKlR0I-(>fgy7pQfKDwpAhrS#NY`q-23`V{<D4NLIV
z7(&S+b^yF8v4@mBz*R3wd(AcMABwIqDo$)tx{=s~lazKX9Tm;2nv=9TioQf1*eNZD
z{uGid>_4s6N}`!lKrSr?4b@tUn0+@gBTi9ai*g@)C>|DtQe+pceuxPfl%X!X!JIds
z!L+4$4PgrS8Mg|MO`dPsUuoKFF&)9CNGdBwdsXnBS(G3Z6GSn3#33=wjokA_5d@c$
zNPaH}8XI1t#3d+vW~f%2CoS9-MiZT<(jvsm)a!@xZWEZ7X9)2Tv=U~;IO9P9MG{bc
zT0EKLlC<7l=Y0y>zf@hJyW)t(dcTRPFi6YY{#j5$@t6;afY~&cA_StqENejWGmr*T
z04=v{xr$3*GYNr=#AQXKyydk_H9!VmgE2HHp2}KOhy&wrYAoSt))gvoREAn0&D<eb
z4p)R6RerR_pA|?Strg@khHH<8cq*l6n(;F3eq)))wmRcU5<7-H#01haN$bn<9O)VR
z7%(^nAtjK&R_zoowplli;s6$(Y&!0~T}X2l2N@VQ;Z@5O&})QFf{Xa3CV`jGPH9&@
zbSm+gtMux{eglfQQ*Jk$xKnMn5>c1%hPCCh5K))(=D;<uTXk0%P*<8{^jQO=YiZ{J
zaLb1c(i16>ZclUnz0x(kyGinu(>9_GW8i|RgOo&55ri!!(ooJtYWG!<zlpGC&}~3o
zde1&@QO=7dKdc;OAeXQ~dw{dWq(f3^uI+|+W&`;re))-5;@_NkR-D{m=KE~gGu+>V
z=<mZ||49h{I=uFs`7_sd{@0^k|7rD4QSTpC|8deQQU$_QOBscyTK(6^*lZH27!9e_
zs!Upv7$GI7xnSBNMqClInJHpzCo$a#y~S3$czPqXm2aaDxgU546gVa1s<{OyAw^yu
zDhP<M@W3}&0#W~T*cuz(pO`SZ^?JEl_n7+Ha+u_P>hyR$5G@KR5ih-+4nD!9+mOV&
zQ9#=`%AHVo@(zk-^o-cqgNCE`>=n-5f8?i2obh@;BY>M|63e!qDdt8;%{0`3hVtKo
z&engf2rjE!L8ARRa&gp-j-Y}BO%W8VeIJre+My(vee{_Rtq5I=j%)Y~*tZ9*>o}L(
z{85*lwf#tC{Yu%S>o8|#o$WZc)bat^rwA>}<Qc!C2|Y#6HFj+kbVbiKbgdn9#o)Om
zJmq1={Sm@R=X!lMr1J{#k<i9#_{`BqhweRcO%<fucFd;J8sI&axz%#~MEmM5P>2Sa
z&+m{a5blZNk&ab8J=ie#dDy7tNX)*fuvIQ+r)jCCT2e=ZzQ9IC<lj1z4->?o@UtS=
z35hq%(^B;p=4#9)(i-}{cnL&l4JwY+IcuaIviS#O;+o3FVU0C9(`#)(X^iH5n}`T<
znZ#f)i{e%uhDL!Z6j^SoL>{Gja7SpsyL`O|7b7}UJ=^DN#c{<BY9J*cK{%6Dv%+Cx
z#0f0vs*BSQbaOiwrybY)?zzJ@6j83#jNbfwWV3GtjOO}J-743P_^KE-#8!4xD9sEI
zp3uOdFje$!_wuThMOx>EKW(D9tLJ~{XLpb5lB>kPHM0S#)pylpv|vHzg^1@3uVp5l
z4rBy8^HF8=8rc!ew+iL<v~Ul^@Ec%y0x%+AQ?aMJGXid{6|o?l%<bAtB?)sU7;G&v
zB##vIPp`~WO*gQ0P>K6NCOnWsgZ<qFBCMh@@~k3Z!y_D5Hg@!9oJsrgE@WUS3+x|E
z2VG6*(;Aks{0x)S#~HWEL<1y5qZb;&f5k7X&C@CbLz?Z5iY1F7iS&0qBkih&*2tTt
zPVqkJBuAf;(gJTx_xdR%r_YY7`vvlpVbL@<!^5O#O+A)QN*Zx$hZ}V4x-!-xHA!=!
zih_})MYkl09S5xh#j!jau?OlYFg7USLEhltCp(2=pNft4Vz5wwGU$>#FBeF+nqgJl
zA1sgj>DZ_(U?|X3H3)20k@kvqqg`t~j;8zw{XEa>D!EsEO_$I-zM}l_&rSX;opt_P
z7@D4<=lk+wnq(@SJ-D|?be{gLG<)2oW_;LL$}IGyC~op0ACw8r-$<PuOO+^apC^Hk
z6~)khB8)7s2piP*T7qiLB2s%KU+*;)gUjY$OFkRRk-#FajVCj2`U{3JhTg(JzC)xQ
z1AF^R**#Q8Wh6&cNutiAO&*qcQu4}pd8m9bOfXj0g15s@alDwcYa`K8l`2ZvyRY0*
zFr)1~NOdiUJ>><adIulQHU^BNK@fV0QESMSyH7ue2wHUI5;O=4!&(6unb^6c>xEG;
ze8?#uR@4+q)$QaSZUHayR75jniqEgUO}a2W(XC9O0J$vzQJF$ni*h5cS$QDeRk<~B
z?3lGss&EZOxsWr#-g6Nr5E`RUps+1bVtt2c6G*GM#5BSxH1ujY!n^?&+VkfM6A8do
zT_#$xu13K!S_zyQ3~UM7SWz+R8{loQzbq@k*JJWCp!Z_3g?`>V8aS{Ta+2>jpI(v)
z)SKyG%&kh_^x(@HX(y*Mrp754pQHZ74}u+oN;BoIXZgrn*b$wuZi&GPO}QIEj-%dy
ztduLv9oP3dss&h}``c^$sw~pC&k+KnOOn`Jo%Cgki-7D4PWwi!0Nn$q@sMTNKdvb*
z2wyC*ezR@J%_!V>C^K9Qr>8+k1qG&?z$iGPy1CXls^cv;#7}w!!Hp{wfAlE6)uHU1
zUF5`y$Bcqq=t{u37-F<UAS(J*$>f!J4G(@eMJxrSSG_b9O6DV=ref7He}?GR%0w-h
zEmZy30rZpf$Q@_KNzi;uqK|q8E}20E`pKSQfR2e@6$J(ed8)v*q{2F6#i$sXL9t^e
z7bjB5A*p5JlxK#Uamb}eO5WoLUy$3d?n9Q;1r-9lWnkvaDZdgSzsi93fR(FyeutH1
zwCF%#=jo>}_{i&6><~{})u%!!G}!u0+S0n<$`vD|H$$Fm&y1QGgrSOy9RZ2n#iB}z
zp#iuY5@k{lXahsfqSPDhQ5)@5AZK2Ti%`)EeRmboYO<Ibuar3%lsH6!bdPxychL<l
z?C??1_@PBf@ZwwRS>QliAfuPzd|)>Rd;JITw(z+dBcWy_^D%0PMQTI%AYN&%DaY9_
zDO18iI(I#(xMWf#E!nBPDVNcs6cKDq2=0lWL@1s)NmB}=OQAtvcMiao?V>hxf}MZB
zG?^Vpg9=zh0@xW~2x?@Q62c9<xe2~bRsa{|k}5!pjv%-O?d|Sjz<foAS?rN8s3XLX
z&e`~J7eGhBtzc=mU`e7NJ_gtS{?hWK{8l`hD&9Il?8^V%TTC~V#><K4WND;eDqalF
z=bm2-Z#1csG}|#=s#TrP3w>4;-;25J5^h}isXF=m>$_3`iX!WdWM9)K7?PliU%;F0
zdR1W9CL!huSVtB7MH=xI%x4Krpp#Fa6U?<4{x+Rt|IJqvlAuX!7!DwM^3M>OL<rmu
zo0M?Z*Z@~-*FCL%C&XRxZRxzmlx9#Hw5YoXvt7h9q(@YUJN@m6d)oAs=$}U(t}n!u
zSLr#6la5IWjyJ7^E(#b4s|pP}DRCTx;rxW|$RnA(bLYson$bHH_s#5-t^%Dxe`wv=
zHYdrqo{YR6*c(Qr)GjDij~y=|wkzwoS6Df+b&C-m<I!8B6MizO7<F;p+`E^@-y&yt
zV-hvZz0F<)8N69#JdR%(ar-yj)T6fuVnh9+Y0{>u*Mbr=aD#P4>&RxLGr)b2nkDgS
zzU9m~oC3N+B^!e5ARjA7c9KAK{eg;yoPJC2ntQFB``}3T;lou8_?LY2D`GgP@0$#@
zeN&zPE+74~wB?^X=wFLng`>D-`{?0=wk+n*r6iz2Ktgjh_3;ta5ugyMJ)!X_jUB>_
zTNq^y3ZUPqNa2BaeeeR=MU~cV@v5`ho;rW?bOB@-$P)I*8DJ6l)^@`ZaMy1(9tC{f
zAIHXM&C90Iw>Ii*Rb^4(;3^%ct=L!?W@MFaSF*9SnkCG@&`FIolU<!Dr<_S*t>~+3
zwX`Z+8s+LJ1^rO)-GEMy3AnL{73I(sq;{(Ru1R!R5SY>w7*tXp_tT(t>IU}m<`RKJ
zp0Y#b!m%f*^51ir#$pSAnKUDVd^8;5b*vMC<C%UFCD8>o6bG|*f?fHC+BV)XfqeE&
z9qIq4+W7D8`nM8HxiN`8zVE!>e33ZP+x15ye#)R|k99y;x?i|Lfn4eI#(b19v$TYi
z_Omi%*gzoOwrHq}pK=M7iCxRly2Itc_|VZBrw<Xb^u9cOuHhsf<Q*h!NnMGd_z<Ju
zsn9FqPvhwfg>(XSD0e@CwU|zJJeXF(_HFIx6eU?#!o0ywB>DJY&*{U>kn7sH=AEbZ
zbGt5GYvJ7cw}mdL(i=I7A<JR~sCSE%YQ~gGJ!G9wrc&7D_@3Oj6Sdl!Fcv7Y3eDy2
zqClF3mE~W<(scRSLM%WhqJ%~@;Et5Z1bDD0QgGH}j1ua_2{PJ&3qc6d7zm(+>0;Q$
zpVdNE$S0CcCB?o~-8trntDy`r&O>_DVqEf5F}dc1xvusUl@ELD&(6!2ObrZiRX2ba
zORSQHF<QmXs06Q-&6H=faW~BQ6&`Pf<IT~EPq&W6d{RlT!1lU-!Pr-skxA+MKf(Q<
zLis-vX#a%qzZ7UiDp<%O$-{FuHEdkg`N(ynMc-bA2O}fU<cTrY<^~l23wF`iDyk-1
zDWVEI<9N?}>G?rai{;@-ze}5QxvYtSAWe`uJWY;sFqs^BzrCC=`Iu2-nhupjS)k7$
zhzfj=KoiH##zg6@^PwYQlENHQN>_svLl<o@fTyUC=Ie{}Y5%aQKX<p^LJFb9Ga}X1
z^jI`vs8@3M1=4%hXyE|`xN+0fk7NPZQ+S(%Y^vF){bJzaA*iBS2@{N)FVpcY#-{Ct
zVy`q75OJUAq9|ReNAXp}y4TjENo%!2H6U|Y+(~biJ^!E9t~08MZtYS-6%YXd>AhE}
zN|#;*1ZmPiM4Bj_1SwLaNs$f#>Am+VQlu9VK`=n*NDIA$eDL1;y$05OzxDmNPgd5<
zB<t)s&&)Y9E3==yGo#B2=G<8ra!qI<G_~I0ja>T3l0>gssY3P%;Hk~?0MVXLV%LDH
z!?vv_vLtAvEbu<*;e_}dj`2sVHtMhG3g^>9#bzdV+8>eap}}u0Q7eAr3PyW)@*1S0
z_ps?V?tW=&Oof9yS(Uqm<J9{CnV%mmX?sg>y5P~3h}Drtgk*7RLc7@LEHsuO0d2jz
z-j@CQ#c>XO%X0y{sg!Td;+I@-NNXrMS`x#_1bK_}a<cetk9}*9-A#?!4iiz!n|tC=
zx9HRsusZ{j?|7NjTdO(-)ro%6zdLCOD`jc45o;nw_X*wf>BA_R-{lRbJ8&BvA2h;M
z$KH9Vv7Sft^&3ALEqs5Yx&$8$Ap1O52&egN${VwAz7D~dhq80n>a@U5pIh4^4#^xR
zt87D_{2KBSj+&#8Rfdyy^dDqBd|>zFJryX;oR(6|PYiPc(yG`m_IZPPnw`OPD6_1}
zml4vQE-veOioYzo{UC5Gcp>_SpJ`5%8kjiEFza`DFoa}dfKNcx#J6=>dLIiQwC`%W
zf9qS*Q-<L63eF^P8C6L*DZNX6VXo$g*W)Y}tH4j>OFz1O`mn#aCt5L0(7n3|DBlz?
z4-2#-jx?pGIuuj{{>6VdtKiAhU5@(tYlW^if5=|HA|V&2JUDQglmq|(jDTl602=_0
z8^F;GK%)Q<P8nz(Aby|#AiKpo$Va!7ni132+rAx}l(4R!oDye95|bE*PBM=>#LKOs
z@unZc#p6?W0H<p#%yqw#xS!aQ{3-cU3JQ$E@B<lR-$W*@J6ddXQi5enH6bz|-r_vx
z$3}5LT|*grDV<KNMZz?c%iNas)`jtDI<?X()CoZpgJOIt>DvT!DWPxgT;7<lu&oI&
z^0F_lyxo`Yf4))un-cx^4FAKB|JSmtzsz#)y$W)U$N$PPghUHniw-$Q_RAbm3b6kF
zIf5G~YqKu%yW(^HImb(F%HNMJkXYaUR*J4!;nV?g$O(EB{dE${@wG6cX`?fe^kWRa
zfP339s);fDmILC@?S$zxaoBK)ZO3CEL+$mqxrPat8vNEN{J8W01Ym5e=)o`TIDef)
z3yep6;LGl}U%vk&h;qYj=qkaNb{5<gc8<K4%NLGzUV=QXPMgNJd~_$`+XN|Ml(C8U
zr2V7;*hD1VN+_sBK7ly20AghZdVWdPuS^t)QG9zW7~e>#HYs~vR%N+W9Bi=af#41X
zCB=rJ7wurOB5qt@iD8A=J!X5$h>{J4s+DGM$bhfNwz~gB&Fmo5U3B~MX4|j=Z1Hp#
zSOEoms_(TDxP74F4`So)XR(sp5$m@*@v&h1$`oZ4i^JroUbf|<(y7%;7uLEh06vJT
z1h)g?2KH^tzUN3Y$7v9$<k#`7L)j8O6gDl$HKeZ^zkuHYul&>$c`Tb2I%UP-%WO4q
ziaW;Q{%xz|Vj_R2p^1Yqa=$mKSsPJ)=k+9-va}l*&(EgZts6z=*or<@5nV>4R}{?o
zmh$PzOFEIJHtba&aEWwHF@BG|z+KR%5nAjtUDS9~Qk0XohJLl^U#0cYxh-l{{gU6R
z7(kY*U|rG>^kjnjVex~Q$?trz3cGhPILM}dVN_E*XB>G!cW<OiI)M+))V*?BT*M<N
zM4-irB06fn&0ks%951adEmYj>@4`#O#kj!mI?`tSSTw<2)Sb7~pjm-0oh1$`ZrF3F
zC4kxcrT)GU=&r+lleb>2gAq5lwNVe-mDWccL^JH{TSmztY80NZ=NeH0Q&B_gDNH+#
zNx%=?qKrhSS7li==hk=cv7uD^&E^RJX|y;;2v`!(NzttNr#g<80=I0Ng;&40vqOId
z!b1IjoBIHYVmmCR)~M26kBO)M__#S^w?*zyIkZYH=7q0ZwYbe>=l&~BGdD#<NL?^x
zyiIeUCgGQwwgRmWkV5%$AxmQKz0pZ+VX}2{(pSFi5`LCZ&=6N3=7yqJRYy&zH{}s(
zDdtR6z3onepFL{N?V|^!wm|N=(;k;D-|5d0sF5p4nv#igCXdG(R;x~`R2+TRS`mhZ
z<7?^Vn~Oa?7oxEJR+n4)AOXAKsN@&oRV*4af*s$_%_mzyPvNh=e~~yK6-vuMJrbI&
zJXtGdth3o{1(w!LYflNAFQgl(ayA`tQG0J%mie3na|_a#p5axVR2^nj-V!1E{#pZA
zxzQsQtD>*z-7__AVlZwuD0z`#s_uE*K79rp+kab@D+tB4?^rGnN;?X=fCtpo>e)Ee
z#qZBFoli|*Y5W4F4eE`1>U*lM6mL~{Z~42y6s(pVyseMdXRwUO7Bz}y;k;*%dyiK=
zTJpq<$4^E!<DIN78m&8&Ln_Q>KvZqsj_P@vwZ6mWS@7`>DUl`dUutfvheDu&2ijG7
z&tkLVi!jghiu7pA$NFqBKu3522(|Ltr{OD0U%wijDFz*a6slol9iU`7#8_6m6v=uU
z_m>O-HBM9JZ&IA!+VshzFlCz&Y`t}O@H68beTHg8gBb$i-})pU5eJ4auD-_rSq2>!
z23|Dttb*8%Gq`)T3-u(K!Xdy+_+;Sm1ygZb6Q&qb^-<#-uhH{u>JCsL5#*<T+g*$^
zn-0*U5mTn{Nj%x+ra+HMXckPeU8+qB6iQ^;P%i1@cNn(0?`ntdGZy~t*mNLgo0}~q
zvn6SKb&qt(usp*qFJprZaeH5z$JZ^Z`S!xBP<(3@IDA_tYO!cDf(~;I^gFyBA-j|C
zxdvfLo)J70wLyz=mIAJ@d~rt9hCv(cpyn8OD3z!HG1YR!^8B&y0gu%}oHu*GtL6|`
zcfTBzl(!+`<fQtwfFui37J1vx*brp<?$fJHw0*}7uK)nw$k4S8$g3d;1DmNp5D<{%
zLs5K$xBR6CigK)4*9C2(>E2i?*gf8sZxh=+jg=WnkzK)EvTcXlb6q{7=o9g8^~Uw(
zmG>0hhe&bL3~$Uq1|o)2L^B$8J-VeqQG*djN0W4rp1~f?%nPT6<99NkwuSCJlxmO*
zfp3)j34naN$L7nywp=r`9U-W8*x{wdo3lY5;6pi!f9mDvvxRm-qwx#%Few#IztiTT
zH-jJuv1P1#rWXJ=*{R%TiOs--+oraXbR(W>G=qZpXoj7kd;I$=8X8XMpqjhgJv{_a
z^9&WpO8f!qejZ?<2>Sg9yByR(2BD43gu_!2>?4q)`U63{1qty7zYr?XIt|Al!o5AN
zf#GK?&<EdlmDev+7`-#4tjD2HIi`ZqjU#25DT-+3P$kC<BNlCRKCOuw@!juhF5Awx
z?Ht}$cTB7j^p#3y_E6wA`hS6zmQ-QE4}(1FKA|{%HMD)NGyRzE3F%9G(UcSuRAo2J
zr9w3ACv={5N^gLs0Zq4qz^WgU(@^vDU$}V5mexOWtLan2?L)0AdyMON^!-$#m}}8B
zKp8AH7h`guJwh7|eG;(VV$a#MdlJupe^>k|78z>XMzZl6qn+GeOY=YR>-o6K`Zow)
zPOgQytI|ibwc%2ccAs`PuN%qY<^0&@jCZ_uKMTX^Ti9D|0?`fQr3;2SMGAHKI4dc&
zOvN&4n`bPOO=zg<L3G?Ix?Qv}T^vuXv~sdD=^Zz*WO{}mKUQ5FUIWa$?oBrM%h)n<
z@fByYWjpAiyLRfrO#+iQ(kku!DomiU{l`lf@0CqVy_T)}aJd8poUy2l`hO6=#xkE8
z#VlAU@HefqR?y=-2WlGls89Mo|4n>GT=&Gw!m6=jX%P;PzAw-%$<50d<^Gl8+mS*3
zOHm1RPrBO7CBKeGBw`XW6ZtX?lU1)?PH;cNiK4G7(_nd)*8?rHbX=d%ZsFK~0|K6I
zX<=yzKNWa=kQKBwhKc7?)uW!kX~?fUTscN-rdI-Np<bS?oY5cVN_Eb&eVo<E2h*b6
z(<<9GH&HUV_!ZsJNH|eAY*s&RIy}^V_{Pzcjoh10?(O0emHm}sW?@b4Q}dIF_7)(#
zU8KIbg7o)94I7UwfCj$Cqi1V$l(afqsZs*THwDETwvFzb2oQ=G`RELF4%*bSugG9J
z>I?<oo&p10<bHg7XCt}g0=67ojhPH?F7+Gl<jRzWjS@pSj&&Qg;c?xReXa#vbM!x{
zaD_87Kfn2QVIz+>z}8wR4icQz;Cjfeq<X3k&iEbFhvg08hNp_K1*g^aF?VLUdRlB_
z)UU-Uw5U{Uu{sw6fCKlY8Vpw{wdxoBHCb4jA5Q=R_D%4@%-lPT#%(fET187Zo>gUO
zCEK?3J|k)xW`!JE(~QVUXeYOhgKU-_wBVDe^7W*JeUR6-GkEt?0__YY=LVz}O9E~`
zjNE-sQD)s7ziYpuO=IJ;7*tFH{j|rP(OzE@2V=^2dM4W&q{EgGCNR_XAP6RWZ^^aX
z2Q}5emCf|6z-n`NFhz!BJS>7uPV>TnW9cZ<Sh^Rr8zdP46M6jZ=zL<FeOrdYf@?Tu
zCeS6E#VRTd_Bw8U<TNe~7RnYC<obeONsO&?%KQ#&yCdmt|2$Cx;R&1UGZ_Na9IO*1
z*_a9t9}!k`XOb0XHy+*+`76;VIOa)LpxS4T`Q`-$0?ShXOzrY%TPyZZI=NITp=pxL
z30#n!a44&pEeeKH#hwue55NK8o_Gdkn@i;Dgi;L&Ny!knHc-Rcefdv2_U@b}VcEJb
z^63qKYMT#Cl_#hm>m*N}A8`|b;W#TO5Hto6HBof`W?6KO1Z|>uN!H5H4nobFqdO_q
z-4+c3&vC`5KE0E}w+Y#OwdkyHf4-hK(5p9dSiX1u_lm3}!O%c2FGDtZcdri)JuO}E
zk0w>KVsrH)I!(sxyJ9qlX4JXT4VYrRqz<$ngS@$B>ko_E-&o7)Gc=uLjjj%seeK+7
z*KEw_K_r|1<}8YOEl=CS`!0*H(3Do5_DdV(TtTeQYqY}4b(4v}^{7byUMWIw31@%f
zZpw&>iBwPx`PSDTp3*0bGWjgTk^vDkaf%9`k3|ZERUMB$X%XW<MKm{~@;ZIb968UW
z&LZS&2j?}_-g^hs9<r9Z9fJ$h`QQJ#UE96RwRP+KB8ab1B#6*f*VJS@$ak}rbI=rg
zKZ9Z_O{Pg)nE1lKR;t;A-M)Vyg60<OP;u#6nAM8g8|hi+;dMv+%E8g2g+AjA^B>&p
z+=_mRRKDbVFB*OdEAmpFEAX#IBpg1Xl5hZzkhpzXE6Q49=aOLgm>we9*zs0qL3Cnx
zxQTx@6xdkD5LuVMH4AKn-tO521}UE1eX-B$N<7}`ldVd@$tmQyHIg7!Z1wodhs-bO
zIPlLqRK7E2YxfKonZ_z6i^Hoc7a1bCD5FU^6im@+=QqwmjI-^NON2IWnL<<-*+*Vy
zXVsNZb!TP~Cd%KMug-y17g%bIUev&|6wr?}aKz$ZBpjMi9iw{RvW^~hd6zA;M5V+!
zsrkPD<n-+h$Tl{fIefy;Rrtr6l724K&RV1UDC16R+QhV5Wt>D}$#3nH%9dC0Y3|jV
zM2>?id@&2goDfan=byG7=1UpPRT{ZW1>8f3;Rlxuc3IpXguEMMfYLeic`R1CNRhlZ
zTs;z5UUjPS#v!x(o_WW{@o=i~H?>)nmHp&W?Oke#K6L`0AK*?o<&D$0pV>^<&EJUW
z9dgS*^<Y>hh*p+*rwGM<$i5$|k+PPPL6-cTfz+U$eexi!Q<~82!{?&j^Nw2%>6Nj|
zY!B8-YI!!Fn#QM;-ZMVlIbTn9asnVew!kwCP2@}{*T=LHTE|%rAf19vy+7SIHdDNG
z;E=M!65VP$&d)eZ{rN!uBcD@4NNE*bg~Uu>&ZN0fa?c~epNl0djbBakOog99bX##(
zM=9NPphoEeqfQKbJmpHk-2xU6z|O7au%5&+&#Yr{MHL?c_=HC5hx$NI@zGKV-50q`
zoV#(&J-LhUG6`lM^fK9E)25$0)5gFdtii)%$=SQsKx|m+CVlU?LHvB@($2?UqoXoy
zyv?nwl(Q2xj9ATqI2hy?3>=!zK~zpZk2s~y2tXF0G!aYz4BzsA!#%!v4fus_+YhND
z91A7Ka?VLTO}?rq@)yu)XsdoFI-F!3<HG745qf>gL~ioN;sCK9RtYK3r{Yy}Fzgdu
z<}`2Jyj5@?MCQuGr%&$sVJAT#arok7D!;8$*0sJ$aV*tbQ(%x8NEg3M11+=JIeO*G
zyr1xf4Z3Z{XG-M?BGk+}%By@HIfNrP*z^SG+PxrtFXHsbmc8PXzxLVOu<R1=+dR<V
zh2>C-m-+z9;`z%{quM7yL8>o3No(jcs455RhU-l4y91RzkPYU(LW}Jx#Hqll^R~9-
zb{3QNjP+XC>*w+Q#A{V{t3l$xb@t%Vhvd`_7K<{-RzPxGXNAdVbv>F)9VG8I(+H+9
zP4y>{L7Jo=@iQb%G3RFb0=mCZ+h9#9O-0Htuti&VEXrcxZ|Uw!Pc1k4jU|q6lm-CK
zD`B(;3ijUt9mPZ22aP^3v2fnpZ)SxILt;_p;Abx=X_kiwE#2yKqYYyhyhyiEK)?2F
z6P>C%g@X4>3)-kHQ1NXqoVgjyhd6387ijWNPLu}-CV9rtjY~6<mxDbKkH7Pjie*c=
z?xs+fNA4Tg1lyCcXFUJeh3A^1V?b@Zr&Pau0-T#ZdgWHH7%h+p6t$iFd=CB9DG~Ms
z!KQc66kk<kr9-?KT?+k8gg`4`7j(?K__ePvM38}_H03YV>}c+$A_ZgL6+2%Sb$52l
zgR#35Bv+g@C8fdC3^e(Li^bgto!xBPx5D4fGNz_srsI6fIo-SnKOo&C8HmgwDYGQE
z4Zg^jJD+zVZAuthVcjNNLxB*MZy2d$yw937AJRA}*%W{uKeO2UM7=zo!#lpc?UX3>
zW^1%Gq)L#VQoZ^Z?_T>BcZbH(Id86$E72=;%2|Y~l22O>?#0egN|V?Kj>JpcgLTV?
zp$67Tx=FP&=8vtX{aFp-3($^)<JVr!)8q;W&1B^C-ETP6Rm)}c@QC3U$NI9HsP@3@
ztDbdOZ3P$0c#{5}do1~M_k5xn`UBEfc5$3idyes0Hx`zt+|BrW7<rJ9CCn3dJM!ym
z`Gc;-if^sD@oTIvz0_>b<#feV1$oI}cK6fX4`b}AFD?km_;?!ou!K0FiqP1QNA(+c
zzfOzLFJ}@^d19Qr+sErj`0CK&?3iL7bMk`6@m!4$C`B}lxV^J{Uf<S(0m5q7<xi4|
zXzhrI`uZ?3^-D@3@ctU+#a$suS8-+jt{&PATkMnharNo*DQ16Q8l65K%!VFxViPNj
zI0SZFn9BgQqd|6K%kFJXW6MqHw}1Dzru+ol*NINRJ|^G{@^OwbNNJ<tv)_w#613m@
zaD;n7b7wJOVETLxl2mhY#6k}NS;YuLymP^(so8^*ZL%Y#jJ<=()8~7${=hQ2ZPl^m
z6{(EuL3faTIYKT*7$h#=tC+ztcXtsFhAY!LlhuXyoMfMy%;DmMn#`efzs<1vWLuGI
z+UJlE^W47-0}%r0SPB05dWXZK+3$&et3{$P<lZiehmRkK?DsZJ?qC_B0lZC>JLoRO
zGsl=p_Inujl}e?s6fn$BkzX@fpT&L`tyJavauF8h*#^e>y9XE&3lDZq_BAiRAc$nO
z-$nO|sX4~8W1l`hqhL2Y_m4+w?L8&ozK{z5JCQ9?Uw(e-jRBWqpY}oYVE88Z**eRP
zfVg@ya9+juAzaewG|3i|^tfAPKY)4fEK(Mc4O^yw5v-^X%Q7&8wO7-q#)Gm9_td@E
z@H{|Jk2^g;xt*1QxmQQ0#)F|q8}mF$mz$<%NS8akTcW_wCz=%#!JGYJR}jcLC+5TS
z1C(CawMX9Bg3fReCZTQ*Qcflt&g4*kKj|D{woSTdKVI!YmCZwkwWK8%&=RSnZSMIM
zP~f3%Aja@OiBo87T2>?fNHu~6R5H%Uj%E9m;svuao8zHbX`}D_Le~ifX-rcqX^!V3
zF$dKH`ZD*X=}1esN|*lVyQK{(ew>uY+t8A4U54|nEd0w)x|lgX-c@Cmm$#05Rp4_H
zW)Z9{w3?8d+Ugahx*4+mt;Km%_5sUF;YsCJI=yvW&wi?8$ESSfHLc5acE%}vF;<Rk
z10GzXeI!{%FN#6v-#%t4q;x01pMji>R1#IsKLnPEzVv}@%7`}QZB`)p3J0r(x~<s2
zyF?m=uY2fu_^h%?A<RmI;cq%t;FGSF#czozFtFvNm?9sUp##{*ji(z?)BVW?I>}2i
z3uzZaqs`Mq8%zRRqv=f3f*JTfqbXtQe8Apf;13J9{n{@~**uPTh&6^V5DM;+p+Ld!
zCby>}s5HaqEFS_3lAy`b$|}0Y=C7^31B-`N+zW3PTzHPHP|o-ZLkXqA_|z4nF_VrW
zbku~{tOg(7#SA;6UCvh2Qkwd-oX(3Jo#d8Z04n&Hx&LFA-~|>YNoJPW7w5<YKb|LO
z&T3Ea9hgvg6r`Sph{9B#;48Az>kiC~-1!kq8^BVq;G9Bi;X;o3?)iu($)lh|)r;Ma
zL?sr^y${jf3iC%71x8DvXU;KU>^ycy4~WU9L=j;H$YsgzhVkAHObWU6@xtgm02;&)
zU?<I62taAf(wzR6NDA84&V_$TY=8`}9wwurk)T|6ufHTk{)#L2`s?wx9sQM;{mrJx
zX7X2b!k>`1T>ZN#l9T-v0xrrwo6i41xFRq9vY`Lx23IEZe`4iw^>2d`<epyH{vbP5
zU76DV34%*1^zUXj3KwspAlnLE)jR%)JC}SZ5(+Zye-i}RZsj^i@#Q8G2r?Od69n02
z<NA@GqC^5g@@ct=fGpL%qP+eD3pEnLHFJ)e7|6=r>!~m?Uc*3U(Qbku3p%e@=RYCF
zj0A!#3BCz|tO2|Z5zLANfvf|)34tshyM90u*snqSEgeKgxZ)6z)m2wAvp<n>X^(b!
zUjJ4UT@#(%gh3W5T}iS2#AmL*V6F+XZnj3Q=)Dp${fW=q*E{hqS<_Yf|DBIFiO{RM
z-#;-f{8#(G=)#+OMXrpwJ`PThTKylB>uT4?^&-~?B&zhET^kDi)7-kkK(1}Lj=?8`
zjPXxX>k0#zCB8nGdS#I@kZK}s9uH&!_Ifuy%OgYl)3mti1~S2UeLxl}T*LTV+I+JY
z$PD5YPxvPyFaQ1HazOr@`u&e1`if{ozH3|ua8mk@w4;_PCg5r>6qhff%eCfbS6lxB
DM^e=H

diff --git a/s-f b/s-f
index 0e04980aa..5ac3f3d27 100755
--- a/s-f
+++ b/s-f
@@ -3,4 +3,4 @@ SCALALIBDIR=/home/psuter/scala/current/lib
 DISTDIR=/home/psuter/guru-svn/funcheck/dist
 LIBDIR=/home/psuter/guru-svn/funcheck/lib
 SCALAHOME=/home/psuter/scala/current
-java -Dscala.home=${SCALAHOME} -classpath ${SCALALIBDIR}/scala-compiler.jar:${SCALALIBDIR}/scala-library.jar:${DISTDIR}/funcheck-plugin.jar:${LIBDIR}/z3.jar scala.tools.nsc.Main -Xplugin:${DISTDIR}/funcheck-plugin.jar $@
+LD_LIBRARY_PATH=/home/psuter/software/z3/lib java -Dscala.home=${SCALAHOME} -classpath ${SCALALIBDIR}/scala-compiler.jar:${SCALALIBDIR}/scala-library.jar:${DISTDIR}/funcheck-plugin.jar:${LIBDIR}/z3.jar scala.tools.nsc.Main -Xplugin:${DISTDIR}/funcheck-plugin.jar $@
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index f01145dae..220d46a05 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -17,18 +17,26 @@ object Analysis {
     //  - all global invariants are satisfied 
     def analyze(program: Program) : Unit = {
         val z3cfg = new Z3Config()
-        //z3cfg.setParamValue("MODEL", "TRUE")
+        z3cfg.setParamValue("MODEL", "true")
         val z3 = new Z3Context(z3cfg)
 
         program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
             val funDef = df.asInstanceOf[FunDef]
             val vc = postconditionVC(funDef)
             if(vc != BooleanLiteral(true)) {
-                println("Verification condition for " + funDef.id + ":")
+                println("Verification condition (post) for " + funDef.id + ":")
                 println(vc)
                 val (z3f,stupidMap) = toZ3Formula(z3, vc)
                 z3.assertCnstr(z3.mkNot(z3f))
-                println("Valid? " + z3.check())
+                //z3.print
+                z3.checkAndGetModel() match {
+                    case (Some(true),m) => {
+                        println("There's a bug! Here's a model for a counter-example:")
+                        m.print
+                    }
+                    case (Some(false),_) => println("Contract satisfied!")
+                    case (None,_) => println("Z3 couldn't run properly or does not know the answer :(")
+                }
             }
         }) 
     }
@@ -40,7 +48,10 @@ object Analysis {
         if(post.isEmpty) {
             BooleanLiteral(true)
         } else {
-            replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get)
+            if(prec.isEmpty)
+                replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get)
+            else
+                Implies(prec.get, replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get))
         }
     }
 
@@ -63,7 +74,21 @@ object Analysis {
             case And(exs) => And(exs.map(rec(_)))
             case Or(exs) => Or(exs.map(rec(_)))
             case Not(e) => Not(rec(e))
-            case BinaryOperator(t1,t2,recons) => recons(rec(t1),rec(t2))
+            case u @ UnaryOperator(t,recons) => {
+              val r = rec(t)
+              if(r != t)
+                recons(r).setType(u.getType)
+              else
+                u
+            }
+            case b @ BinaryOperator(t1,t2,recons) => {
+              val r1 = rec(t1)
+              val r2 = rec(t2)
+              if(r1 != t1 || r2 != t2)
+                recons(r1,r2).setType(b.getType)
+              else
+                b
+            }
             case _ => ex
         }
 
@@ -89,6 +114,7 @@ object Analysis {
             case Or(exs) => z3.mkOr(exs.map(rec(_)) : _*)
             case Not(Equals(l,r)) => z3.mkDistinct(rec(l),rec(r))
             case Not(e) => z3.mkNot(rec(e))
+            case Implies(l,r) => z3.mkImplies(rec(l), rec(r))
             case IntLiteral(v) => z3.mkInt(v, intSort)
             case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
             case Equals(l,r) => z3.mkEq(rec(l),rec(r))
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index c96723707..99a6074b5 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -72,6 +72,7 @@ object PrettyPrinter {
     case Or(exprs) => ppNary(sb, exprs, " \u2228 ", lvl)             // \lor
     case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl)    // \neq
     case Not(expr) => ppUnary(sb, expr, "\u00AC", lvl)               // \neg
+    case Implies(l,r) => ppBinary(sb, l, r, "==>", lvl)              
     case UMinus(expr) => ppUnary(sb, expr, "-", lvl)
     case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
     case IntLiteral(v) => sb.append(v)
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index e6bbcaf74..8d617a834 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -54,6 +54,10 @@ object Trees {
         if(and == null) None else Some(and.exprs)
   }
 
+  class And(val exprs: Seq[Expr]) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
+
   object Or {
     def apply(exprs: Seq[Expr]) : Or = new Or(exprs)
 
@@ -68,12 +72,22 @@ object Trees {
         if(or == null) None else Some(or.exprs)
   }
 
-  class And(val exprs: Seq[Expr]) extends Expr
-  class Or(val exprs: Seq[Expr]) extends Expr
-  case class Not(expr: Expr) extends Expr 
+  class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
+
+  case class Implies(left: Expr, right: Expr) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
+
+  case class Not(expr: Expr) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
 
   /* Maybe we should split this one depending on types? */
-  case class Equals(left: Expr, right: Expr) extends Expr  
+  case class Equals(left: Expr, right: Expr) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
   
   /* Literals */
   case class Variable(id: Identifier) extends Expr {
@@ -88,8 +102,12 @@ object Trees {
     val value: T
   }
 
-  case class IntLiteral(value: Int) extends Literal[Int] 
-  case class BooleanLiteral(value: Boolean) extends Literal[Boolean] 
+  case class IntLiteral(value: Int) extends Literal[Int] with FixedType {
+    val fixedType = Int32Type
+  }
+  case class BooleanLiteral(value: Boolean) extends Literal[Boolean] with FixedType {
+    val fixedType = BooleanType
+  }
   case class StringLiteral(value: String) extends Literal[String]
 
   case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr
@@ -142,7 +160,7 @@ object Trees {
 
   case class MapGet(map: Expr, key: Expr) extends Expr 
   case class MapUnion(map1: Expr, map2: Expr) extends Expr 
-  case class MapDiffrence(map: Expr, keys: Expr) extends Expr 
+  case class MapDifference(map: Expr, keys: Expr) extends Expr 
 
   /* List operations */
   case class NilList(baseType: TypeTree) extends Expr 
@@ -152,24 +170,41 @@ object Trees {
   case class Concat(list1: Expr, list2: Expr) extends Expr 
   case class ListAt(list: Expr, index: Expr) extends Expr 
 
+  object UnaryOperator {
+    def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
+      case IsEmptySet(t) => Some((t,IsEmptySet))
+      case SetCardinality(t) => Some((t,SetCardinality))
+      case Car(t) => Some((t,Car))
+      case Cdr(t) => Some((t,Cdr))
+      case _ => None
+    }
+  }
+
   object BinaryOperator {
     def unapply(expr: Expr) : Option[(Expr,Expr,(Expr,Expr)=>Expr)] = expr match {
-        case Equals(t1,t2) => Some((t1,t2,Equals))
-        case Plus(t1,t2) => Some((t1,t2,Plus))
-        case Minus(t1,t2) => Some((t1,t2,Minus))
-        case Times(t1,t2) => Some((t1,t2,Times))
-        case Division(t1,t2) => Some((t1,t2,Division))
-        case LessThan(t1,t2) => Some((t1,t2,LessThan))
-        case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
-        case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
-        case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
-        case ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
-        case SetEquals(t1,t2) => Some((t1,t2,SetEquals))
-        case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
-        case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
-        case SetUnion(t1,t2) => Some((t1,t2,SetUnion))
-        case SetDifference(t1,t2) => Some((t1,t2,SetDifference))
-        case _ => None
+      case Equals(t1,t2) => Some((t1,t2,Equals))
+      case Implies(t1,t2) => Some((t1,t2,Implies))
+      case Plus(t1,t2) => Some((t1,t2,Plus))
+      case Minus(t1,t2) => Some((t1,t2,Minus))
+      case Times(t1,t2) => Some((t1,t2,Times))
+      case Division(t1,t2) => Some((t1,t2,Division))
+      case LessThan(t1,t2) => Some((t1,t2,LessThan))
+      case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
+      case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
+      case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
+      case ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
+      case SetEquals(t1,t2) => Some((t1,t2,SetEquals))
+      case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
+      case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
+      case SetUnion(t1,t2) => Some((t1,t2,SetUnion))
+      case SetDifference(t1,t2) => Some((t1,t2,SetDifference))
+      case SingletonMap(t1,t2) => Some((t1,t2,SingletonMap))
+      case MapGet(t1,t2) => Some((t1,t2,MapGet))
+      case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
+      case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
+      case Concat(t1,t2) => Some((t1,t2,Concat))
+      case ListAt(t1,t2) => Some((t1,t2,ListAt))
+      case _ => None
     }
   }
 }
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 1e7c115bd..caadcd2f8 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -8,7 +8,7 @@ object TypeTrees {
   trait Typed {
     self =>
 
-    var _type: Option[TypeTree] = None
+    private var _type: Option[TypeTree] = None
 
     def getType: TypeTree = _type match {
       case None => NoType
@@ -21,6 +21,15 @@ object TypeTrees {
     }
   }
 
+  trait FixedType extends Typed {
+    self =>
+
+    val fixedType: TypeTree
+    override def getType: TypeTree = fixedType
+    override def setType(tt2: TypeTree) : self.type = this
+  }
+    
+
   sealed abstract class TypeTree {
     override def toString: String = PrettyPrinter(this)
   }
diff --git a/testcases/IntOperations.scala b/testcases/IntOperations.scala
index 03256597c..0c79ac4cc 100644
--- a/testcases/IntOperations.scala
+++ b/testcases/IntOperations.scala
@@ -1,6 +1,6 @@
 object IntOperations {
     def sum(a: Int, b: Int) : Int = {
-        a + (if(b < 0) -b else b)
+        require(b >= 0)
+        a + b
     } ensuring(_ >= a)
-
 }
-- 
GitLab