From 09a5e4453a9dede98b4a033775112c3b5bfb573b Mon Sep 17 00:00:00 2001 From: dewert99 Date: Thu, 25 Jul 2024 12:36:22 -0700 Subject: [PATCH] Update sessions --- .../heapsort_generic/why3session.xml | 73 ++++++++++++++++ .../heapsort_generic/why3shapes.gz | Bin 8035 -> 8413 bytes .../iterators/06_map_precond/why3session.xml | 43 ++++++++++ .../iterators/06_map_precond/why3shapes.gz | Bin 8357 -> 8595 bytes .../list_reversal_lasso/why3session.xml | 78 ++++++++++++++++++ .../list_reversal_lasso/why3shapes.gz | Bin 9387 -> 9737 bytes 6 files changed, 194 insertions(+) diff --git a/creusot/tests/should_succeed/heapsort_generic/why3session.xml b/creusot/tests/should_succeed/heapsort_generic/why3session.xml index 418185b583..a3a76cd0a4 100644 --- a/creusot/tests/should_succeed/heapsort_generic/why3session.xml +++ b/creusot/tests/should_succeed/heapsort_generic/why3session.xml @@ -7,12 +7,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -248,6 +309,18 @@ + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz b/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz index f21c225fb597c34314fe438780146c389d1f3872..6baaeee80c7b804e7cc1f93e07b95a9e71b040e7 100644 GIT binary patch literal 8413 zcmV<3AR^x%iwFP!00000|LuKSZ`;V0?z?|Q-uj&07@$_&>!7;SUJF)DbTNXuDty@*COVwJ;|M~IF=imLO{Q1q7eEa$O z=Hvf+qu>1ae=qJX@`q1%|GH`(UfliNUw{1a1FhNH3;(l^A3j~ZzxnM4wx%`r|9@R52MXm+9{4Ia}ylEjf7vk4ZOR<({`5(90-{sp06unm4XPf?d zbD_q7)LM5aCs54Vt%+@Vxy^;$T$nK&+ch79u(&rB3)rTOV0uAJB|&^mV#@^t=zqH# zJ^QcQKXcz*^jG}t#ea?=$u+5t#Rg0sJs5#e{gs^3qt|2xP~P8-9*m%v{z~r<1A(|P zTkrGe*$7fEb+T_a6OFAoMEdW8o?z+DfA-hycVr!mod%!$ZT@(NpW~L7{-@!iYyAEh zkMR9__MfiGt*;-;hOFlpW0svWj>FIz%^vcf+^sekL=f6mwKS9|9de;qNG=J5Xt z{3Ep2zizPgOOe&J*!^&Ik#*O0&HHP!7X7te%l=xeRevql7(ieF{U3k3``u%~zkh%8 zkE;(iDZl@LuZ_RExw`&%=Rf#={=hCfAAB!ctfTyLx1}Mt)sfXfvzFj;8b6Vwr$5n?5`15O*gCc>RB> zRQOap9QXKwQfZ$JS0CT%YnrZOF4kPmDV6rY2u!cSxtP+U)?CjimG;31O0U1U+9AfQ zxm{2y?XwZ2UiN%DAMwKtG>m8^w=nGmZJwl@KXtcZq3E)a#NG7vTJYg50VFB^vl4h6 zE3(=E%eppO#Mmx&GOs^IZ8V7g z(qQdiSM@Yc0c#p=+I_zBw|B!%7bBfFU=jWNUq;;`jXSnV@MHc5Fx>s?Q+|UR{`T5` zyt{y6{(STPOYWb8>;FcFkNLK}fnQ%P-rwAO8g}~0$1#R2e=Xg;!XMtfn5z2;6LIcl z52?S1&73^|Y%Szb&}zGO2^_`3Wu1$1$otlP8~^|x;J&|Aa%57y#AiS_y>JUNCRS(>MA=2TMNDo+w*GDbG>tmK6Ev~`HBdh*59Iij# z-}Rb&@blMxX7n>Jvc~)l`=skH*LBC~P59TF|H-#E1N&T2RNHkGZvOn3K6^AB>C{cD z3;fN$<=ZzmU-E4Mu@~Dp*`lK5zW$e=cjVS}+Oo$d{P8w~9}@TDl-DZY2^nI()fUKK zrtQ1dv;#`+Yr6_|I2g{QE!ifsWfAn?PW2Yr?VF$MKLOGe@{Nf^a)W_igZpQ!^vbhXd2z zQ&R^$HMo>Bo|>?oyLr5)ChWVBhdNw7@Jn}N<*h3)@53FT7Fl&$do9KeXfbwJEz$_! zVU^zt+RX~OYVJAR#5*;9yl&#}Mv8x=oA}$sZN=8?Ebm6{aRbYa>%fn6_x>{Nw&+rg z*5B6gRK4SQB{lfFY_25iP8@G* z^dpB4eU(w!5ZH%p)w^$?jeYwT!MtZb6wh+IZMe}QxgI09J|b)|V_frHwr!^YgBh8N zV`Bv~l#PJ03^%v8H~+}#hY$b1MOdys`s+lS7-Ii(H4H%}$4UU+J)H3ym%&cqs0AqO z0BLdu%LWdbH6Gp7b=s2Oa&wOkKaI8FtYte5;PoQ_%m0kO`;WinnL#-k%IWxbY;3;< zr$W9DIdyp7_rI>wApYGf4*nFtcQ>N`k3aYLQ%*j9&q4H&k3#|oL(B=|z{bF-!Vpg>3~_H^ zjCR6?r{?WkJoeQ5L>6X_+8-*6KPH>_o7n1DxA*vsy!_lPBG<0-s)Z+|r5=57)j z^0)ESX~v7+MgufGY&ia-9dI{{%*CiS_yF~YM zrB6ce6mH^7cE#hliN|JSY~93tSs730T-3eX$Cg9CKfLG~pvC3ke2QW717{19yowL^ z+3eB6*)YBI!n;59ATaZ61+4kWY9Tt52JRcbi_CRU!XZG21)FWmaU!ry<^+-4XYJn&S5U7Cqq zodKy1A9(5!zypWYQg7F;TsrVHa|fQL(|yMuc$#-3Z8KX1uG(|2u$p61O8)Ne2M&!z^S zU8}9;R(8nn0FT0>{WGZn=0?EWGO(=$P&HMdPsv&fbJ^AF3G?gH2(Oi#{8n9=<3sdD z&9TsItvjtzlPsV@>er0cXa}M{chpO)Zd=SugRT0n($mu%roH-qky^m1($|Y=Pp1H# zOgi19pKC=}tqw*1)(;e$k7<#-n4MmTkQ#8`O)^pk9;@>P5w%UQ`Y$Jk_AW zQ|}a4+hKjD*_2i5?SPTiMh>-D5cvX){m7k2Wtx^z_7shjH1?usTgm$a=a zohdj~P3dOWRrOc0zY;TbqPyjuqIobCR4w*2%I zppi&D25Yz2er(<4(Wdx39MQEM*GtgkEMl|X_E$`7dd-$ZbVO|W&*ZG_Yy8t}>m|w5 z9(&4nCy&kcl$2lQf-{Wc-Ea*4ZMM;Fg@ssd z+16(s%DGV!S7^E)K1nECoQ{XK!BkW z335{yW_yooyOG(!z1$IqXsg4Hb^S)jY7VcR+0xvDtV!hU;siSzhAv~8_UW$Ewr=+7yAyYVCNw`P zy{%?Fk+6w2?rrE*zkjj4UbdaX)+1JFuSHza{Y^Ib&HHrqWxH*5MRuFTQ=iGJ{sk1h z!?3HP7fhq*TaN@lU7>SZF4WW>O~B2W@jvz#svj)w{&lzKtA8x-sN<4TMucMeS$;o$+C`U91pf5{8P$ln~5|xZpZs79f-Nv za;Uh9&kqnka)9_u>C60y-*H1T%D-C1x^G-~932H7Gbq#K`k6sFL{Bp!d^#e(jJj{U zy=@R6CP9E0=1j;2@b=8T{%VD{Yp=ds?7*CHPe)YD_=`&o7o1amz-^p77sCw2r4$f# z*wpi($2*?^GKI3^1x!fW#j=63o5P?s+}xwXPN~m5vbYa`j0^h%_X2j$e3n@#r{mvp zGIghR1$`fahN&iMkZGcZNls4ye8()$IEM0oS>Ed}@u|PWTYu>xIl7B5=gj|!kTx#E z=g;}}P_g%^NNVZRqk$Tfg&!6A91nXwFuEKSHV(qRwzTo>-=;fskHO}`y4zLwCyqLP z*K09vB_0g)#2tx;<6Tx;M{Zy|kc58MBeDnXcRY}gbyJl&bGpB~Z_&O!;6B?U52j6x zXjA)XQ~hp=6i4i)JeathqwhyY(B(3GjWsc=)0$KH{#ZD&jW*M#Z1X&H#XPY}IC?|r zp?oZAo|zDEAFhYe(LOlUuSomzi1)iWS6|5#K81%e^U{!0L9yX>@zZ-K>~d!7R&KX$ z59Vz>vU(HMUD|zh&%AOMU)S)+5p72p#m?~XuVHx9QyU)DncHt>c+|V0z26!hb$X)h z8LP|Fl-QXveBY4uT-iKk3;qT2T~lFS2cLSFj{JHQ)_fpwIZA?_xE|)v(ZUN9(+T?? zFNE_~sPgP9;d4+uwOAtY0vVrGdFFCdpEgl>_U-b!?p~yfW}@>4l}DYa7>>;#cx?vZ zMQ(M?<#?RPW-V}2Y^^qBC3W+;ruN~ktc61dIa~zL5Pnj}j=OeaY5Vp<_sCQC8M6Mc z60I|1cB-X-~AYs4E`u}5qq zQV=B&vkHHdu_dw~P5tSG=GLMSi52k`;exH)%C5{xuhdGe#EM_!9C#9przBGn=olge z%?hz3O_8j@kqyO|L(*C$YkA7dWWhslT)L25+sJ2TDHi6HjLMJ{(P*bErvPayrdmjz zrJO7|p^Gdu z@&HiTG7{Xj=z>yQxsp`ISo;LMWk?hfpfOwPn?^2z1TVl4t}Kzw!f?iMp&igSkXAyk zgjxv*O{@f830euZ;%>$5iklVJE3Q^tt~g}MSDaRyt;ns&uE?xNuSl&(UZ`TNa8(>e zL|bsJxYI#si9r-9J{~42IXM}*@k;1med1DUo4F`Cc&_p}V#4qj@3P|DIcJJy#@fVe zCX8NG!aN=(YqHK-3x)M(B@l#AOt#J@Wi2KXFkyN;4lb^M%G;Pz2-X$I&9NLY&!ZPc zMgB(em86vfYi=d%N|?vN8;f+pVkJad7pw?aYfkH+Sjk?3M+p@nS5iC)cEw{726})b zfex&3pL}!>gf51A+hDgVX;xA{AsJc3psWmulGFjJgX=;iMi-10T9q*w?g=R=(2|yl zNzjB$SwYTds8&n_MVgbYlqk7UVx{;>(MqwWrN?qCUsq({l9}XvNV& z6-T74&=^IdWV490Txs!@=;6?gEHOugM`NRbxl=Hs#q$EC!cs%e*Ck09X*mqDPb_m2 zbRt`{kJUr*O#Af4n3d5hqgF<)j93}IGPE*mrQJ%~m4>sTpKQ@NvTzWLQHBTDd`DSE z7-gxni133N+U&O@Pr&(eoOpoaqGi;v(kkI|8LksgZ!B9G_bn-`18a?PE^Eo87K}M& z;N&n(+Gx!xg;uVtSXsWZ^v&pWE<`U~gst;l!L&=}E!D5!;yssk*fCEb!OpCjc6 z!HQ*>F@!u(@(>*_$rXVxvhm`pi|f?N>E`cqqTC2U-Z55qHdZ6DL1chs$;gnmLBwt` zI`d5FCl8m6c(rc`@gw6Av%bb>ws;MfrI|Bs<(@GM+#|qef=oe#AZ2zOF+Uju3m6pP z*k-jpZ!WAd9%h?(EHPm2Xe?p48@4bNoOh~nL5!UNCr)V}G-FX3!F6!Oz~C2X`&8G6 zO?5F7t9woD_jBgOXas;NFt`J-Scn11!0+=C3q4syvK^Jmi#Qve3Oq2QLA`>{lSq++ zBN3b?m#l!TYu1Z8JGOWNV;b>|$u>E!Q_RIjDU#FG?W9f<6O(7fmW7-_Sw~DEPb3)e($ZhI%A37%dPbx(i{Q$ECUOckBnY3#SUB5UmK3b+ zNJm?e&x~}gg)?ydiX@dKuDP+!F|KeEOSh9c;5|?Bv#)0&91AkpD2xg=+7L1S$ub-2 znZ}TO041&tkWWAg?;RgZGvK9)xMHrTD{dfvI)*e{Ss}eraBPd@I=KWBuCz>oatuwp zhAbEBW&;S~pW zTey(9G~VVInWz(=85rMo0CeXlJX%LYS=5Fx4yi_ST zm|p3E%7rCYTtYAh(xK^MvMQDxDVUck37&oMo}0)8C7ygNJPDIbHcqLMTS=JukzLjg zIr)+WqLWWi3CkoyoP!C$JZa6mP+nuAgc*U<9TkvBre3p05)4=+@JhPUhR(X)LuU=Z z8UQo^=!y*O>R#tTA%5dcpYLLQlAzByn?z1tv7A^DMnJ1cgnTL~XRSR_tTn=|-i@ov z8~1EQ1Wc9nDpm`87EmnOS=oKp`?W2#-^T5ndXVYGZ@Mr2>_tj3uxzbE7_E$@qLP)I zmIsHnQZlNG_oytYGa#7zG@^|Te zYv~4Ef=FB-u<;J=ZxrClS?*)5hUuQt{jMzssThotCq&8!9~6fSd0|GC7z~T`sJ2R$ zgF((J0QMRbC4vTF98a+bxYjvoo1ImNH>ARiHbI;-K*9LG5|IcNVieAKTa?f6P-Kiw zM{N=!52`5!RV1%YEXDd%k9UQmnms9f&P1{ZOBU0HnN8*euP3?Z#Txu2k3pBF=#m*L zq1MCI9H*GFNjXhYH8?ZFRE;xam=r9xs)Z`BEO5rP5s05{@J{l`ofzeIaAwb$*T|KQ z#C71xB7~DhM$fb4Lg=96W^k#lXLs(rQZ`;fb$ew^NF`}lH6gPzmGhL+DE;CE@S8L2 zcP@#?9PpQ<1<{(KXWCGXes8+TVSZnjV`-&!!4)nwgynsa(ZJIA61~a}WPF#_NN*TQ zIx0<6;0I|HbtxVZHsjhvRp`64##PO#mV;;=MPaPgFYx3ooNLA-%xT##t@`Y>1R=?J z$4e$mtpouCA)|(~t+-{`b0xk@YP-2*7##0li_BRCGARh}Y|)ZTF*$#iRKFo3T!3D0 z-YCIJNjVyu1K2d#)nme@(w~b825^9e0}ro=DyE96;;P6hwu-L7hjtYsP$F2y2kn5B zQ8%XiSMYbJ@L`fn&~d@wB9P;|1;`qzgtMs_|ZP76pf7D7su~ zegwzzYZv6#poqLnnJ0$8GUg~06Iu$Fowf`URH<4!%_}Xk&J)0be)xLS39S$frl^Qz zT~D07(FyZd)WQ)fV^`Vz4GE+I9g7)`s4eltF{wHHSEF%gjs@MlBZPyZZ%3q-&IQQo8HJNGed{e2Ll3irNS?^e~DFmkh z59l(hTP}?$RcNo!Uh(J3hP80Xq^fUmLfoZ_2+nH>qE+xk8r8B<{cZK!S;+{6iq54f zaG4bgiCc*nr7B1)VAHZ<&V?OY-${lzu6m1t%UUm~SvInGn073bmK}ReEJ5`nA~N-5 zb&l)j_>jvGKvIjR*X=3%omvH?8iENbSL4+h&EV^ay ztXbqWHV~R22+mHKj93Q$r;rOnL>gRwZhPKr`da^<$YKOp7T&~WG?Q@L22PRMk<>4N z)f`I6scvp529G)+tWwTVa5*8OSA45(UIe=_S_@lFQt)C$EW(Q<6GB{*m6FuFu!tM< zG3ZkXH}y9yuwsBv1EIz(ZN4%q!9uebreM~2sA-=*2UFkK2^Z1@+Y~MEy5V8;Ik00$ z8|G>qdx4XM03;|=-+xPRRs!_+Yw2UsRtngIpo>oR)io5NXxTbT)?$eeu%#Fmyg{UCqBN8lRbSJ#?3r_B5hO-tJVJvg@gK_!cFjpw z&jt(6ttq$m+}RW|*{oxI@id$=8yNs3BZ`Xk&EB#p+T#xW9r`=;cj)iX-=TlCc@B6S z@K|>)EJx2vKGvOUR79WF;eu<)} z@8`j|*Mkqzih@K#mWh|F5+Md?MM1Ac9N9^!xlbujlA@5$%m-z?4#H?5SSyZKB@(V; zeT7_LiAq#KQw?^VanV^>GH-Io1=-J9M8;C~m@MM|2R=#-G&;IB(1dX{DLmU9HP&Gv+-*_^;BfKvdc z0M6Gcu3WdW1t+JRY^6_9ISM%=N`iPGOjr$VowP2uqT}Diw-7iLDk5fHt9mi*eAbci#A3#( zEY77?eB!$ZmqqBKM0oC<2*nkVye(ES3mGb7>t=o{Lit^c`^EUbjE@*@j_UvbI8k&S literal 8035 zcmV-pADrMHiwFP!00000|Lr|%kJ~ts-}_hO+uY6K09KL3$6;oG#$j^~u(*6#_~SPC zobgUL@;5R%!n2$5)?z^B?o4SD*9Er_J?; z|9qui{rK+}w}1DW51)U4wRnBufA;bH$E$bOzy2WButxu1SAYKdAO79n{m=F1o33Sl z0h2CjExF5I@~2PR7HWGT-;7$ywc?ileUtrdzL`MLYuY{A_Sf4B8Uv!W?odvkn6+Dj z*!FVU3%k8AV>q^JJ_cd=-c&5iHf#mc3t}n>z%|Gn7c4;k>+R^-UvK`%eRtVk;p>b4 z8ADQQppL}`OddTLfua6NP3h5VFas#>ZbuJBP)vWN_lRMExG`Jr^61$JQZIF|ueTFT ztdT|fUxS{^(yjmGH|=*69gMvOAN@`KaLYf(Eie5~!$%wb{WCw}@87cjcvWtE1yNh) z59x+V+Vu)BNN63Qqm{9}~**Z$q7ylKDMJHPl%Z9 zs#&G|vJ`b)c0XKQaNV_CV}EVdvcJ}A)nC(^`fIi3!DNig%ZFcYfAfsx-Mj05T)n?e z`P~n=HvabdYV+aNzxV(AL0opo_nWoU%C+es%k^$>aqXrPPYjkzqetqE-MZuI%T+C-YhP2f@z

; zvqg;U!sjNh+hyjaNVaQC!ht2L*HTW_?9X#eHi`c(tmoR`O{X4Y9nnUE_|Fa24t7;l z^Aw1t;kMnUTYqyq>~t~Ge*+e|pa0XSTZD1PRv~`K|6mNa|N59;@eO~o@gHt4SV@1n ze)l=|&zbALafc82roF+xK3}}MzWzAu^plTc3_Jc>x_jk6yn8WK{SzkQ+|3?Re-WEG zdj!~8s*|AAcI^^4iG|BL7uAsWzp(6oj5wA*9;J>>q>k=P9UY|(4vg3Db#Q+l4Q|ya zi;WMD=s{x>^Zf4sZxHTmG@ zn|@~WGcSt9{0{r1&F4+sZ+aE}_3Hof&Go=OR}|HDU4`pEKBP~cn~rqqw$%my&A;ZG zSJ$8OO<`g$c5|{t1sT|ef_B5pfZPQuXo~(*`=1+bDr#pcgc-!`vaRWCnXGuQS*5jLhYi`aqUMscV zm~S?msXKUm>TTO&&eYVs<0FOx8zN`61AgXc_pTn&Y#cq~Aa#NCY5vhP;Ag_%&OTD@ zb0TSQC)!|2+@4p_9&iK8p6h@ox_f_`c3X6*M(c0qcvA0p zUMbD|T{c&W?NEEgJU4sMS9OBUxd(OV#=qO1yo#>;hkv!#YKyJ?3C*JxE^eKm_LpuR zwPc`bz2M6o-|@H2yR__?UJiEtk5Sn${`Q+O-g440a2H9O%wN}|clR0s+f%Z7HEw@NZPJeXmYX|t_-U*SXD!=#05@L%SpH}H&42hc&kV}RP|nA{XJh*{I2H0;$f?8o zuK%@3gZOv5IPf8W?{7pOLb98O9ZbGa!F@h-fHfA=A)oC$)N|3*nUKyq+B^?g4Nf17 z?h5?0aIG1Z%TcU6v)$gbY6IPg9U54vi-G;R7+JQ9so}dAn#GH;$-Ed?Q@j|M*^7bs zy%?C~i-EarFySKcUw-c4Lry-t;~@Hox%cZelw<0-s)?{GBX=5B%*^0)QWVaAK! zMFTKBY&U&Q&dI{{%*990jy8w4{rO!g}5N_g3 zcEy)-6Hm>^*tv;^vN9gfxu|=&Us?|R{_vt}z%4G1=Ti)uA30l?YiBZMs>$3@r)KV`W0^anF&kzTsw0Ot$~?%Jt(C2)dn%6P5vjZ6 z5h*tUeI$=a?ed7!k$l4QSbf+e#B-O-v12&ePnbG$q^U`=qQxYuFC$e(@U}%Wb0S5f z#H@Cy9b8yrdww)Q>&!t|OsqU(+xV0mUUusT3;*z0bDLps^uUt_yEGHKIs=l9A9(5! zz$1s&O7GULS~~DFa|fQL(|xBOc$&8(Z8Kkvxmrf=I0J=AuEoqW*s1?2Jw44~I;j5_sbx4-`g$?#=^UVwNvE4UDXsP< zomK}Y-Fe8@nlbK@U-Y7|`O&FP%dTEj4C+N;P%nyudQmy37gd7_Pa0Hs>b*j1JFM?C z+Y)QNyD9;#sryoGy`EG_*0Sv7!cJ_fOGkyBx~UHBu3%Dg3A?J&nSxVlN;kW% z)L*IoO3u`Y?w5PY=D}1@wb;{)3p;BC=(N>-iS@2>d{Sbq`#MzJlvqz{DQhL@Y++~f zUr% za;k@gqGni@ZVwfTqMI!gMK@b0if%0@#(G>R+B9hL&K8_kY(TdeWuhw-HB%%#Q*B(` z+xn}fAhfMUT}!#~fBoa*yDVlJ3}W-z(*MHWaX*%>YP+pt;j6wvzpFiO)G#ZhR!dca zX;k~(bZIL<4ivMR$w1B&vzn%u)yxlaYe-ua)l_Y?JAX}y>XIuqEE;GeQjfvfEw&$9 zcX_laJ`YEBZO8QzFgc6ZuD8P#6Wd<1B@rDF+x{~-Ylj;DG~0SfGPTEn^4$rft!e%B`_uBm$~4K$MJSJ2LCbJXurZjF1Kv!Gmqum(8Lv* z?uSnj3Kys2vF-5X=hInol5;fyF@KV@1$baI7o*$h;nXgFx(9kVoLqw36o%Q}dO)dh=l;q-}kAWwJ^`jM%-H$aDU*Lhnv2ld^VyFnA0zbL(}W<8Uzi8k(S z=vBXevAbTjox|26R^gyUT+;nbHu&|sboF_+ZFU8Am&H?`sjL146urZ+ucH@CqwHIc z1OQ#3b6YOd)E-U1&6)Av4;QK*FLK$;-aYAM2lMAnO;N?LkoTm@ijE&{e>tOyaqC;U z*Q`K3UEkd1bahh?X_tM1WA4eaj%XYYu_yd<%4wU4G&gRi`zjrXx!H28xC-Y72u~a! zoGE>oKk++lXh!*0%UBPM3&zn=;3+S7=067T)|jC(qwV#Z%wYPjH>;t{uT@>~ux6qiy!=(wrJp~pL)0WyWM z=LJki+sCqnv!BC2TW;>qVXxHZ4q4nsK*ojrfja@aV?N6)l=JcLIGMUr`+~j;LBmuN z8f2Q#Fv;lwfbW^*8OKl^G0O-2C7k+8*!oNN$;X`;RGcOG}7nB%o7eBm*A}(jPZq;t<_GsSL7glewx=Z`7 z?wMEa^6MHNHKOeVqu3c9{2GRb9@_9wXKufl;i0!fd%rV0bbg}k6IPe!DX}NY@LfaJ zr^@CjTky}2@0tqxGWgWPbmW(#u;v4a%TW^a#Pu-8juxJwn9kVucqW{`K$T}-2%m%M zsl^hBXUO=h$}^Xv`m~A4v#*!mb@wb~G!vcQt32w7is94@f|q6xp5<28T#mQ65(k^4$oN$w?A5?2ydQmoLe(5}#|P_K|ys8+~8 zYwHz?6}T1H6_^$170?RQ3giV6B#KAB_ACNLKlPHHrUNd z>6M}fBqPfh$f}SaDIG$#s0)-BT`*c|Dq}M215#3g(iVzIJmCdd3C`${9Zv)Tji4(f zBv*thf)$CCat}+7#T>jVDxeZ3c|!myDOGavNU`LG9@`LOR>bRvR-_)BDq%e)BLYCC zNXqkEm4TvgnaELSsM4^~Vnyz2&_hYGKB+Us`ka-Z;sCUjnn%%)Y8H`}D~(@?9?XOy z2?qtEvC%jlI1j3LEUZ*SYUug8BuS$zVj!PHMiX=bTeOc=8GE69dS&#=(8{Qlkt>5M z11lp|+O4!*Y1YhorRl*IodZjR#*o2akmZ(Dl#T~Z%NQXvw3%;5o-|H51PqB)vx+)a zT9sn$ggPOM&aI67mK4^3wT7I_S_!445Kfq4tn2puQE}F@_ECm?wHptj5MyDSs{ovVU1FZHWs6EZ?*+l zB4es<(MvT#3m$2pTJo5wNaH6tnNtXwjduF>8PbM?D-W1loem2vCau3zR63s zlRCqDoaASpq+*&?N;XPE!A2V*&wsGO20>%;87QDSLOwh0{HfnO%_`oCxMHrTD{e;q za13eoWTo;%?AI2BI=RFqoU}?3atuwl28;k?{T5YC0#+6o5+nMSi$F)~BXI1a0K6#L zM0Q{kK}5mMICXB|<0PK-W}P!7$)d7hbCn~9^D&_{P;3sZ*yZD8fb|ZqVWou5$!5!L zxGsvP4NslwS*R|81IE;RJvRD*J-p)B+met&FT=u^kZoM7W_Wz4Gjm z#ze}8KqjRE#(6NYXq_83j`0Dbt>2HF9pMB>PtkeHGs}`vrLemsbq0qnyLNCYJMJm5 zRfuO7FL|9QDeDp?9at9&n<^3xdf}GV2ZD-ik@{aAgERx*}jVWN=md9p~1Q<8e zdB_AjG4?|Muu%`_!N49V#x};sPJkF|^mSy+c*k+9?K?V}iJIB5u zviT@l#i*3Y);GByK=mV@3(J8D2G4fHYo+R;mMry9Ul(#A*wCC%12KDq&y96&QEQTh z*K-Kknc!F_3*(CmDQn0r>)g7Y%G0xzf@9OGT%cS;a>XSM=9mT6bTL_qWlswFxk>`F z58k7RC?R3;v0#!WnQRDJxzKiuif~cYlK_98^`x-#lwi|Nk(P8iq$ec%TO%0v$FfHFlt-T zejB@Y>H($~zv;f{(Tfyf5ZPMCVKf;Fg_2bWf@0D- zp@?s^`Qa!SN*(`~ArdJO?18Ryv70HVeOR+xH<6Y^XCQmA# zGk_}6g5_x=%r^4^>q+j@VvYSJ&x5W^(IpE}0!Xwq$0??4Qcjap4HSBqs__IF=4ojo z)jAcnEbNSHBRPJy!8?T!ogC$MpfFFF*NCJepbkiuLpWtr^q3V&sROC);6h!`_Nns< z*?7gO+mkgRm899KNtKt;ilpewWm4bIS;J zyn`(&X9{3aklxv%6_{dj{w}Hhh$saoz(*Zj;vi0ikZPi$ChtK+fLebqYuLhgkP#tc z!iuWms>mv~imu|T2pf#tuHs~*94qsO+c92b#K@Sjx)8wan%aK22(=2GNF-kiHIm~n z(jtXuOo=(8>dNww8AkcAqt?Z`g<#WB zckhQlrs&%dsg?86unCfmO2~GujcN&fB*bQyg?FVC0w-AwbM$2b+ERrolQG>}1Rf2&wnV~0GRf#e49*nR)LOgf zcwPkPgiDW#W+qs=#Ezv&I;$jeECq9&!L@>mLchEo7uiYaxV&Nr31DcMCKo%K#6n?i7!VKT}rYP{W;QsVZ+?Fk+$ z8`fGNMfD9n>~vF+!FjEia0(m;8*16$exx2dE1CV^qI0PVTxAj=p;aIo1<4E8w5;f- z!j2U-13T2!Ta>73v78p!D2}ytT_`O(<|(nns$ZCB(CHA-6=@?l4pB@{Sa{**mL>bt z*dpyrQbrqy9Aprf3?ik(AsJ&34z`JitR48na5cjv_Y_zYmWtLXq#}jNCbM4&PO<%F zqvNe>Yzx-inJ3B~yP>2()c3ow>lZ*~LmGn&Ns3r>%ifb_5o>H9wcsc?J2IJL8UB|- zE`lS{;QB+mr_H9X#m@;WkD$oXo7jwIk`8S^h|rECJqK2EC?#|BrQb%bLXqVzZ8+=KT2_OnqM?yO1u}CSx7zhKHf2z>WcJgsVl&g`F%8Kmr*lk;9~- zw3BVfY#E+qc-5OXb@$FZB^K+NGQNl;Wb>BEzyV>bDM*qzG^LFPEw{J$l-Sbs4O@`4 z@-bTBATJ^hqfWMv+O@f;dN#s7&c*seL{>cLRK+?sN0o;sUSC7X5R zAWyMVW}{#r$;d*HCn~9?VhbJjcii7`f5-hD_jlaC+C0a2Y&{aOPle^^u~bf_N5iI% zqSM8p<00lCgHY@;PMm#iyekUPb4;ird)|rwqpBlrj8WvBHVyCSo-O|d*@pw`V~E-W z7J@8M7M2Ls*Z7rYyHARG&L^G=%So4Pc$B5~wMN|P92JP-YK~cb8DRBXIjrW7SP>%a(n0GBHB30%R##P)y3n_8luy)DgG*G5pc|q30-y`f?T?_j>RFnjk1{EHYrp zlz?M^MiliG@GnCg*(s&brxYM5S-@xE16i+wG+Ij0isMCz1S!_{hXs+KL<$;eui;}K$f9fna59r2R-#TreRY8duOtIuf1W=q2L>W55L2(! zOOjJo9J6JpWjA|E$9+TR-)=^;|jRa zz2#dn{O_W=NJ*oKj->L2|GHG77g;rLxaOd?*`8n{&!S-!&NwCGl#KJGiYwQxY>8P# zLhsm!Nh=E(Ej%jkWh*Xbza~QtE!}q!_9EmZSh#`l#-mQcdY6(_NuUTW3v-ePn?zID zim;}e)_l{KB}S8Zt$HchsQ}WR>VZpAr3i53yvJ6IRaEZ#>>F&PhX6rxY@dvXtmsGv zk|Jc%Y$QAk#P)s0O=p~R9Qj%8QcU$F_NBxqRaP!4YfXub=xR>*_gS|WFlMWKQsf}y z%uy1HiG|5lLtCe;%dP0(yZ9CYrvgRBjJ2ebr=8C_3QQtqwh_g-)QS(ki*Q+lJ}M5+ ly_2E1B9phplCUg8GPZ8!w<46^#duhZ{|}D^s_+En008 + + + + + @@ -129,6 +134,14 @@ + + + + + + + + @@ -270,6 +283,12 @@ + + + + + + @@ -328,22 +347,38 @@ + + + + + + + + + + + + + + + + @@ -370,12 +405,20 @@ + + + + + + + + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz index 7936a3fe5302d723cdd500e0c7438988303be44f..ef3ff7d08630f60e3d6ba00987923918137c2fd4 100644 GIT binary patch delta 8473 zcmV+!A?DttL6bv&ABzY8000000RQcMU2o+!(&oK?Mc-w&2Ltf?Q0Zg=}+;vi0RD6*}P|U$hZA?=RdM$coCt4_-h@s?a z>;+zKb=jhS3hKX~#!4P2t3NOZy#4@K0h~X7{?va7@izBgx^=!l%uCx+r$ zrfZq1W$1MaOiy4I7z%j3#LI{)vy6uc7$cQVc3^XNFhz5BP>mNz@iu<`)#XvZ*j?Yn z&n|tr3BTkwb$kk+Fy;RH%g-MpU}|?0|K)CPJ_U4tdZMO3FneHTduW@+rZir+D+92= z`1YYj?dS}Y7mD(K22w!ifr*)eO3w=1X$IIhKe7-$KIw@~rh2@PH;$TkU;ep*WK6US zGceXDl#Gm75RSNN?K&OgFi(^{%<}}g>$5)0Os5W_VNKa^rfL{dHiSKN%WbjUAYtbQM2{4{4>Bipu_rCt07Gi5qzTYS~&Y!09Si zVvvzWA5fF~YbN3*Nzqk2Re8HP8d(gBM9s_wIigwE8Tdz3)|i=u7N#4^cr9bKj9x8( z@d?ZVLjliMc-18AGiR!MQe4>H{IV$hFmkVdE@FXhzr%l9zNJ+bM3n_V$4LJ5&i(bn z|8_qg@DCq&!F|4VH+gtCnY0PdLo^7$ZTy%nwno$aBia@MGF-l%fXsB+n;a@DAE-KcWYsPeB?-}+?r zZCgc7r)6UMg_ptsb4N0s^`Tx{!_u%l>v##O|~r50;ipdFQCF8y;>wxe>yZ~Q9C zQO*q~+yo={%lx`RiHmY_XVIpeTcF=FU$%W**|PsZqZU7Y@9@tz!hTHhT9joW zvTFr3El0Kq5uB|0E+0^)d#ZU$F<)+BKL~PvAwXg7iy-&blF^P4q=_HwuS=Kre;2de zsFBU+Hs%bakDoI^mK-C!y0oT28ZFwXQYZFGYr!ohsemz$dd zh2F{ZEwV5$09^!-Hkf|gD6)Tho%285obSX9AGChA!-iY-_2q-M`sLcV-(y2Ta&Oxh zavp?JS)t5BuD@hHy2E_WgX|c~e-#XiDZIyWv}HL#PG&i*6<^PC8Q(#$%5s@rR_J9D zZ)KSpSdO(Uwwoo@1mOtaN!&%RFE3#^@}%~o->eLc3=U~;p!6t0#pa_ORI zsx^k%r__R6YYfOwMZVSwtIZ<1vspw-&da!0L=R?SC`$LXicD!y(|V>Sa;SSTX0fru z%1+R@OEW+5`o!9OA->u-e_|!+X1S3hYg4(}CsMhqHIZoAF{0~~o6V6>L()x~;bYr0 zniIB=RJ)lZY8kI(td>3B7LuAW0OpJ!T}U$ro_BJlyp`$6*1aK8_l9iU@h2twr3Gdu zFbfRB=F<`{XVY#xt4LY1yT$M48nMn}r|r&6)Bk%#70>=q9Lv^d z5tdEQrYLRFkdDyMe*{TaV20pG3#AQ{x8>KHSVt7Ai224y{{6w$_fW3WME2<21xwen zxj7CGam40OY{udibryl#hEt9OBiETaZNuXc&~J`<1#BF&6G>WHNiFE(=F)MZCJXHz zRl5e;ccJNcTGfh#rD=DsCtH@@6S@EL6cIZv#79N=a+|)!e_UL4ed+(U@3tJ_lN8%1Ye@!@>u^qRSOg5iNX=AdKO)=Sg&UU$DVRv>c>=36P zw=D2We@#*HHU zf9zE&#?#ut+cS`?S)C}&%hSExzJu7_>pO^i?Zdl+T%1T|hpGTY-BDbwD5_mhur#T9 z9#b{vF=>0{Mb@@-=gy0KE|Ha^m1T7iW#fF>yWU-0=+LMhp5*IO@Vs0qvE0Sh_0{}T z4|UV_5{$BXtq)T!z?r(D@v?=z*c7*Ae>JTey>$B&{LWfCu4MDY1ntcPti76mwRaP+ z_HqK&-cG>U>k0CS#Bsjz5@;`{A8*T<$3aHeybV8|GH;ihvJKDKuw7i4L{<*sGw1NR zaNeL^u4|l6fEG9k0=~km>e=%OOfC27xo!+ej^((V;~ZXtd1Bd%9$wT;1zu;0SE}9iO&6i*lH6GMR7bc)L+$xT2G|3?m`g+0OsVjlyV2s7E$x z=cZal@%GEdyNkcN@aZQE9K3^^ll%-fe-;(C>da8{u{5qHKUe-ZER5Iv2D|Xmg4Y&& zlZuw!9IqN~5*T2A51RA;zt7kVHbEVYE;VqCfoLV?1u+Mt3*u&oNtFNVXm<8!)>ANvnvp?upHf3sR1 z7O3&<2Y2)DR(CIoSN>V`Rlbkvp4^_PXA9@&d#xU~FxrN7{qgI_x8gItf;`9ot-a z!Mg9XNQ^YL=Gi$>)v85VTFTl|f4-{4vr&ufJgL$`)fQ@Zo~9W+ACB9doL9E`{%p04 z=XEAtKGdO>60ZvgU0>^0iGSs@SBd{U&%{=|P9Klgy~_40N4?7S?_ee#4m!Vz@+$+q zit_JZCT39{&ISyrUGsiQ*^QW@PS3HEvJWtClJ9`StAozhmW_NWo;~ww{_3+K%$#Yh`WX=W>We9$`5!^@98Pg8PS( z`dyDj%6684+^U5-eqydE8u{rV`ItUMlcl2OLKMlU>R~$lQl74w`cqjWC!`gVHm|l3 zlJ;YCq8UNijNpbGf1%HtQl#_EURi_|5~Swu=+%$yt;C0}J_$wZC!y#nS(lbsE6LCE zrubRES`QSf& zx#@4W-nW96FW7z8V3SQkJ84&^Hl4kZI^IZKtG8q$b*t3xvI3atu-vHHnolWJZ88S4QgStu3<5SL$Q8l`}&)_T5FR*WychB;)m4d=xw%ar5PWx1`~RjzDi({-h@ zi0?_j3V;Dr`Ao!b`M$N^rX%n9<%$7^2ESDfr1uy!+llk*a-l7$3~HyVcggaM*|>!1 zN02^!f8}))8#CB~i=llSz{}-w`k1CyPjC9rQoP5I`IPI{TAaV$)|$?&8vMK!;>WDT z4|nIXYL&|q#s6y1J-l2${4RS0o4SX$2dda;@h@~w{jMqJ@2^(8SWY!9m1T3evYtP{ zv>LzR*knbjGSaFxXX7ECdmLio#pxz>{a?I*FCnpQSnNd676TVxSU{rZ$#0_pe2P7k z(8KtHY4|Yn49LS~Lv-}Y8h-!8El&Y2MqpItp z9`Y}aaab6woReLS#{qjl^_>K4a!kZYj>-HXP2S#gz`w#VIfcrq9?7uK_H9$AHsk5gvoY!8+*}`hia`;Ol zk+bmYYQq0mt_T^P-^O-CsRGu$a3dhv#KSQ<3pT02UW<(hh}dmoZznln_QvZJD-yrZn6_(?k3 znND}Albz^z$1b8sjw@iZ6o5Gqz2$}l9;6Qd8%_dZ6HC@J7A%h@XitRbv5Z<7oD4x_ za=Gp}?>Or?o=L}S$4tj`$5h8;f5$|}0El&rc8qk?cGPrKcT`<~E*b<8FvwmeBRYA%ChQ4+`%e~2bBrCB7=^~sA~3P=vq%5W``Dsn>fS&%BNan5P)lOhC? z+)L%HBFgtlIl^KgRh=K1GmL8*+;i!o}g0<}_r zPHky#dvAE`xy_Pb#92_9nDo*~6&!QI2+9c6L`cc*FZKgX;yi}g`+#lf&dD-a)ok6}!Q#{l4ckxPcj|i@89WQ0f7e#4&V^V7M-0<%du=^d zRW5ogUtnGj4Q41WY->AfI(r@pfocQaDG}i*tn1)iA8qK35t1Y+Jto?A$n6rkN=b?Yn9^vno{IV%L0 z3^s$OUJKz|e~eUeO&N>a@UtZx_DrP46DAy&D!J6_AdPW`^h8=Zun9jSf`bc$U{tyH z@T2=+y*2RAG>uNWp8ApC^BQIN=1{{{(j2>plH&icFG%nRTYR(tJ;!EuLdLQRk`5;Wii+AvzOa z7E}0}f2lVlVwu*WP$yoBx)>EK31)pVve!NBL8O8!-20dWEfxOqoYZc)9ma%&|>a^yOF-DAYtXED5qPStqNx@a3W$Yw-De5GV1dey~PUSED zCL4jcCsy`W6K98+eKEdc!UXF~qMGzv2}-2ue_1pN0-~VW%BsmC;&?0n6MYX7dcRsWrC@oWUz^*qEWbdDe9o>V6G9arA;uC zVcP>LgENKMg#pc8nmP+IdS$&LUS!(=0s_&9Fzg|_gEpowMV*LA0j-C%D=d-PS=j5` ze@B?|LbE^%b>yX}OORNhr06LY3Z|kXK?bcbk|reWRhe1+V$@{^I4C%23iD_=O_ms# zxPf`;(@33pv6)R$G2a__34OAGC-{$4rJx9B_+PP6M4nlj<6a(DDa6|OCn8@ zXTMcQWh|DAy!ytT%Ob);z9fYqKrQ#l5O@oQYWNV&OGuBi&S?{h3WP61;mp_3eT^4;wx@P^xXrKBAXw}7O^~w(C1u-!QNNJ*ZfwZt38YX0#9EW6)bl$aHgrI!c$|1x%|cyM8bRF z0#%x`z|aH^q+~H=rwocXQ(%Ece*>fjNDYu0Wg2A)s1;DFoZ|x23aAz8Db!P_r%+F! zo3(t8-zftH=tYdC?e}Fz9(!(fbuuHx<0m%`sl2E>P)-t9YCB|thBJ&YiKhFtM z?AwyiM-O#~{<2^+Cp|Gfn-nk{1KdIJhC%Z%XdVX5!=QN>G!KL3`IbcW5&V?nGm%H) zeMot4p=Tl`9R)M&4J#RVK$_F=avolO{*DCNUIt;EcJQira5MzNfAF6q9M?){G7<se|hDk`RuC*G9`VfsKa+V(f%C`;Kt< zkrFzx4_0t)S%8Tef0Sl2I<18rc^@u2<3PrNjLR1xG!Ph=$wH?Rs}ze|5!MG8lC;Ll z0779QF_=gUHqto|Y-k`xD`$z1u@5N%xyJZfBWzw92VE?33NjGD$YX*HEOADifceEm z>|+A$!9*oQ-%Bb$ue|9g4Hde|wc0~U!Is+To zYM~NUF2V)V%vxgM>q<>v0a`i;tprk$J7vzgGbvg4a@6`{VZXvDb}%4?(D0<-2XQ@i z2Eb+hKY&a6yXhR16#fa!^;WV(rAx#b=6qJLA~-vC4v1tvjv#-x9p#unIEOKsm~%{Z zN^nJTBERyif44>t3nKgl27iG`^B>V^XIRei(i*O7aJ>)cHvAv~lZFb{)3MX^Kd$3k z!|DvZQ!o`IK}`o+KG4WXf^DjDn4e|;GV4_Mm<&E9gOADJV>0-dOy~C?2|gx+kI7U% zj)QveF&TVJmVM08uOteZIiI(Iy=!}u^Vf2~CqP#xf38YOAi2=q2{^;tDPpY^TFa~x zF&&I}(c8R{$qe8c;5Wc;@^9eRnZBH-g+UaOSa31y>IlD4CFrH#m?xOX!F9wqFpLAk zI53O@vjAdIZt{sDbOL@hGw6ho@WWDIi7@50&=7zWbdS0uQXeb{IY`AYw2uLaF_BKl zNQpG?fAB&tlESpn2o8*)M4d1W2Gfvaa-6V~lb<@ahXqu>QeM#*iAx zp=gO#%E+9=927OG^p}HgIQWKxZ#ejdgKs$ahJ$Z7_=baTfChj0TvZ+)5N*wcf&G|5 zu+H_#(cU;|mGB&fF!X>N&XmCjekyn^gi->ge}`8bgG{mJi69*8RwI;Qwk+fvG62gK ze*i++laWcxmzD`rmQOz%Pu**s~!7yI@rS=kfqw**X*8Q3T&J*exL@ zGa^*aij;7{qvr4(87w1~Y{uyXM2M-Vm>-eqXGg3ZPnn;ipuOPAL=36)`OcW$q`=4F ze`T2$hxjt5=9>_rbO7&DD3&Nl;*sU)Ri@_wew!eJ7sMGI{+jOIU3Dsr$CLkX{di+l_=2lRmoi!#Te%<~lGn0yY(V^QYi7_Pd&JNf~L zl##&l4wUA;hm9b6&%o#CLP5d43Poh_UBEHu4f*$_2l0at#3%tXd6|R# z*apcW6JgwPw&{F4kGF4b|LJ~?w{L!p zpKq@}-Tc=Z_2%vWytwoBzNH0rcaS(s|WmWsrO#qw&&DF0;Ej~S{0~;Rbfdc85o11u> zLCb@l%Ikxg9^}!gKlB=;7c)8VOiz=x9ei|!z zpsfDDAn^Ks17HPk{`~n<|0TrR+<)o*^rr&_7IUB@a#Eidiffs!WvZ5;*DWwTfmvWE z;PnzOBQE~*^WDGkFacwv(#Z~N?hdAC?hdN)0x90c&%e4n3K+ZVyZG6qFE`vm-T78u_?)TkYuf$~C8 z{=b0~5PD!@=AhEE0(Y7LHqMVMgpW^pVw0&JFXWA*Cf=9-T|qJ?T80@IYZOXG#w-X& zT($N^sr{h{X`LE!m?zC1<~c(j>a#w~45$vGVN=;~scM*1H;iB!KCmklK>4-~pjmt% z1cMrX$iK+tBuso)6Of_N)!2dQNmo&XD3Ml@si>l`c#`$0nZ!X3u9mIk0-UZgCI)$F zbOSZHzh)wCk{Vq_Rh74!qmf0jNY~7GkSUr4pMjS|Ws{j=Xg|A==7E)RT?@u5KEf>G43F>9aQPwwXr zRnRgxcl*WP#$Ucfup1f#lAECMI2>GE-qR${i|lgdr(C}%l~T9CbLIY$fq#rQ|G4{q z=Rnz|`^&r1{{7`Oi7EX0x-E;U_EdRTrRX?zzHO_> z>0}~z)wgV)WPN(7`j*Glx2@`X_PO*ksPFlSRrM{Z`es#qi|16|qNwlLRnr@~Jge(% zU7p`S?`B=jNvq3QDIGnVMys!MIbG>;T6HC(=l)cvPuB!o{|(2|J3$XIw>$TxzkV1=>+L=F&fBWjiWI{Kl`M9Oc|_ zQjXx<>qW~MVynqRRpY1>76bEcdz5A>0g3FI&_Z2n)!glIqvl(S=5A-}>BFw+d=?~I zYT38&mnPGP*hym+Q6@r;o0no4ATD*lK}#<_@~B zy18I&c5~TmcNeThXWqi#G`!_o-lAbKM(?%?82($V2754yTkMy2s&=FmUZ)xF43+m+4AkhcDEWf zY|f)Hiw)C;Z#;A z^N{N=nUC%;-}4|l#&QLJ!(s~Wu^eq#PLPvX4z}X!SuW!{2v%7x)5{9IY~rmfQv=Jf zmgTl&Xka-(9?f#27qP)@nYFhVZI|WQ18Pp?TtGYJIWvFyl*{Zr=#>kk_mtbSAUmqk z)V&19+SSnum8MQtY3eytn#vg&GpjVU&JmQv)sT-d3zepJRhoK#0)NR}{*pWVC3pEt zZmxi|gR+?)e{TKe{F!OCn(f)wX?uya6SdhYuePtp77I*nj+VmJ@7wowZdw#i0&*F(X#(#Tq~jnGcgpUdrL*8w5VHrrYCZ!YcXcAu*1qq(6~x7 zKk@p++I1nmS~p^UWdqJ~AxYMzaXu%uZt1$Z zrRSXrUqW5r`t|x28n>TvzG=u)-djP=;@uWj2;9Z(^zX2x;QHntALHGp8yA~5rSbL> zI$jN1oA%b%<3=_qP5L$7Z?Nrv9BVNT$%BjQbreL~({^R1>Hoc=if4Z)j_uZH5tc>I zrYLRFkdDxQ&?HG$V20#K3#Cnyx8>KHSVt7AjQPe${{6w$_fW34iR{t43zn{Db8{RX z;)uMRnu4W}GSMy_}2v<;7EK)*Ta6|iy8P9$mRCAFZByGzH3nmn|7RP8!! z--V{*+p1P1EM2>MJ=yZ~p2+=|r-;~bAwDX?m)rDzHSXfF>&y7JeYX_|pQPw6w^ZeB zh>$Vtasc}Z4p@V$T*>yrh;K*A1AF`m=Dmqn@gQ478}uoxm(yAv9p7Snxad{c++JFJ&mF7Gb) zvphC`P5z?{*<-dM=c&w1c6god@%nQieu%T#ng#Ybn=d$n&D<$?fK3q1ZWLn^z4^S^yCBN!A4bv2heuJm&&{C<_3ilbl7U?wy~q?4PIX z`;Oy$G(G)!p^^4o{28;zIk*uat539lri~W>m#2%}Eh?hbkkH)2T5IQBB@GE*)3~fq z%d#NCj~#zrR2yfyE{5@XHkH@IO`PXL%@=T~e!Kgy(z^wAUg z4NOHYpE4J^j`PvEXseBLQLjC?KPw_HUzG#qCo}Zb*7DT$BL8tA+OkJ+I=?=DzJv?!`IC@@W`p2t+p zc}&_~f04B<-MRlFpG#!rXl1c3qAZ+GYuCHhg$|AC;Yq$e1<%U`6U$X>U0=;l^-wo$ zFT^O;Ykin<0nSv5#>*1+Vo}_G7He7;dg=Bl_#In2TC(|Kg7#(t)?Q7(+Peu@dpQAX zZzo{w^#u7u;y7Q~1lr5#$J=t|agY%&B7fFvsN_=kOZL6U$ok@S^Ti;B}^2_`H3Aug`^! zaw9S?BW&GKcf*F5O;veX)2U;k?%NQR%f)of3#}C?DVte0y?Cq!-Nj#B`1BJ74$(p0k_|V1MisW|%uw^OG_EHtBZ@Z)E%fkHQdvj;e8C zLKik*%)G5s``}HCrt2USC>*N|DtH9js^I)$IBYvUr|bB!|3DVXw|y~xtL4E!jc-4= zn}4^udr`cK&uXmleN^`p_Dnrn1V7))dfdWk8|?by?Z~&{Grod6$QNqU4cOmeRt-e27ZR2^JiI-1x zsHMc~0z%i<`c>jz`RrBVf6p_qm9Nvs^L4MX{mN0Vvi&=liHDQUucG|QK(C_wJD7=C zl!vnc!`7~OJ*BKhOj)PrSV`Fjm>0=+z~R+F=WEP`T!A_$bGaaY76n(EeY!fPv<}K1 zH2FGph3+1Ny+0WsI?#i}e{7h5+>26tkaCZu4vMXyOM6gH5Q4{371%+E(^&oSz)#@o zX9D^|N^^M|wE<=u|W4pP1IEw1GrQnvV}4ae`gS#j}EEzy3dK{lHb zA9n$d-nf8AKm7upVLf-~OxeCT?~_=6T`RvFcj1jU`PXWH%?`+R&!TGgjnDfWW!|a$ zIbPoYu={xZ|1$GWHfp`)mv3yrWaYM=x+k<9<;9oF+Kr#fAr^Ur<-pVn?&k~cA4=+X zJr-NGvkc@`E!6RIb4}66PY=n*^eLJw6?HE}k&LPyrqeIw>8hzel{IogS}|$&)iy%X zewa=)BPg4H5!{d?^m$W?biUaui_k)X)cj4o`r*Bm_|VlSp=kXi6kToBrDfL2=I8lx zuKJ|vPH0+pLaTb)7cCcqwZQ6`o&|=wJGw2MCUMdRwA}4AP&syl;ejZag;8Xn-Q&&O z_1(WegpZ$YzkH6Q6_}^Cym!3qp_bF9@Ys&HvUWRvY`!jxRx43?jM4Y+FSo_@a?KqN zcV^=BQEO)1bG$(%BXh$$clQYlcXwd!Ptzj}?KLoO4_Tt}M{TyMjt?PUHG6&Y!GHR4 z)8B5rZv`)3u=}pTCYufIq_s}%cJ@Zft+sv_3t*kPJ#W{-&XT%BN2illlV)M9KB2=UdJjkBoX;#(&9~6lr_tRuo*nfk0vNC(?pPe+ zdlIk$U;tG<6Y*QVZ|%3~$a{XdV!)xnZd6LypG*dqDM_1Z)aS#7Tk4{2@)=-gLmfA}~3H%Bmj8wt74T#`{5I=4*cz zbk>+m-S6%AUakDRrN(T&4lM_bS&j2T3RlC}np-xS+u66B&t5k_Xq!bLO(x~+0)_3`$ljUr)t>c%uxD|`c zIMYd*8l031!LJ?yS67yD)Gzk|y`Pd!tR8x1Y?ZHMC11%0CcfH#_5O1CZn(I7SvcNE zQbmtV*RxDSvC?ELleKJ(_gP`TA1=CBc5L)!*}B71`TH5qoK$&#al!i_EDe8}aIGDs z%5qJ;*1ZqOGR@f=DmuzL$~sCrN;=z_PIs!4o#=Rn(vDn2ksMcyC`*0lIT5|(h6Ns^ z4}cm@fngI%)-x6?k0xkOgy>-(tqe|vphSkjRmWM!X~#*&Y{yK;bjMW3WXD9u0E%^t zc8qk?cGPrKcT{y$UVttd1QCBRS_gtyVur{lmDM`&7<>UPJI18`I!QEYE`wxI62+KNL2((0pz&+rTS~Q$JW3-ur(lU>JatJ4 zZjy^6l?f!Kld_Ydlf09xleCkh6Sfnk6S@l<5?>Q*}yqN_2{Migk*1igeO;5~Bb*)ze88(L|;+izK=} zdC^M&`C(cau0>LVv=D!F7PLxhoO9ayqzHjP_fmPQi1NKsj<7h;D$jyeB9ed{_Cf|P z95Ip8Ap3}66(n*`3k$HbAXP>v$QZR&fm$g*sJ67Xy*E7e+!k>#{47XKOnT|03XVBp z1Z9M3BBW$_RC_NAsp2e1)zD%DV<|9@!6lNsbv}jw(rM2%FQk8-3$Hq9xpz>!J`pWQ z?`TjeXw@^vEjuStB^Nd-B737K7oJ5YLQ1mt8Wb}scOD|9ZGcvVbaCp1 zhASxWJM}${4B>_^X4cAcp;kpHzyY?`*2BPZ(Zi5|fjxf|nW21OUDH|J+4E2fR2xK8 zi3m^OZU^uBXhUy|kR(az$)IiN8BrXVqBeTrJx!7X!?XkA=12-oIeu4)?HLgbPliH2 z7&zcDIHf$dkTfYkyM>wSC!#4K=S4W2TOqh)@E$z%S_tQ2q>^jOSmcJEE#dHNA~l{c z;kZ=ErCxsrX^b`){)K`knX_yhNLls*| zb4DXdihto}kl<}#MA$SDeRlkjvt%9-JfjFXqIN-9ji`fL?X@G8pDp1`d+0m_pNQTh z91R5XeS{a!iO?QSQXw1&D1%hyG*QkIw>K?qnJuo!SM;AFtbGA+Q#N^*;`{Kx)CJ5pouv!e{@s}bmMg=c`S)YvTbx(UxsSwciJ|@BV5O8t!Qsi;?{=}Im zc=UgmW7jK$G2UzAwF(GfhtYdE^0elWF-DAYtXED5qPStqNx@a3!{|x+QshY@3F7DI zoys5RO*R5~Pps^%CeDtN`(nJugbCJ}L^bKT5|l{QvuG5gL_x(3HjlrUh1=JoMtFT0B zXW?^mAK{J*%|c0qQ}_%oL|%g23MEBPVKSJCjszLB!dRM+v{%FAsuv?K$FV^n)KY(# zO3P`o#K2Dt%uAmp^7M;MZjy@m-oV%IlMOr}45TUrML5GhgU7=2E^La3$_H;_(87PDK6oY0 zgG$9r3XtWVWAJn~*@8uwY7zRpn_&zAWC=mPl>loG&wy|uq*1|gCj)1iYAQT6cAU;{ zOhP2Q7cNkxISUNU5LZeTQx4UjkqZe1cr;*Yz|?@L0aKw&0k_IKS%6ysw?bWodJ6Rv z>M7Kds3%cR>I+Kp@G5N;0ziN2iF7U*Zi!Ir2E)vf|o;L`ODRBs*B&V>>$`kyPIGDjO zGVJa!fM?YAAV(SMCFjg*n71H8atf9&k>11C4s=*)&K}M8BPluJRT6*7_s&|zw4;dC zwH1;12<2BuVrU2Lhrj$U>EKM@&)`qvPvKAE5A_JgAL^031uO5t0v-!I7W8BdWI>Mw zJr?v>&|^W5CD|SIPzs9mEEvs6PmIsj6>d~Oh$P-HNFRgrF-RYS^s!77r0-i2)kh3z zPFzGDiT5GpjCs#QN;-cEX4o56_L>1{-f#vrQJ%jefwq@HSf?Gr3?3W}!7%(^5{_%c z;A9{$Z;s2mv@W zu@n64JHioIN$GVTtl-?T09P$2&17_13p?^YB3OnXn{goH;zbAz1g=)HP^!c##UfXP z^+ARtt?@E|P)#S>j{tLyFM58slq?upvk_=wi4z41NxSqr(Ip zSmKO20SAN&MB#r4vWu0blMq~H!o?8;4Qe`2XxyTXb~{3 za6KJ5jX2>yt>YXKzYe`qa1|s$Z3kaI(8x)GZ>mb#o8|Z_D^j?YeDDM`A;w}V$4ID`W2`Z*(%uOKdfX{utrc3!tnVDQ@m?MrkLWGS!hQEARC!f{J`FDb(;?*u!~abPQ95V{l3+0kl6Yi!dX+(Fj6g<^Atd0? zI_2*f5Zcs7L{g$hC<3VpBC#Z>lL>BGaz=j^*PgR{q7T4wf|cddYncf8tb}k2cU>nR zGPl9Q3O>T`h4w*Y3SZt0;%YAX>~=xoVaus9oJ;E9xHvdvPG?hJ>Xk!wz?F~L<#TpC z(`k2AN`flGe}*QaU_kS+FD39_3bF5vG{d<=z<`P1FcBOkg2P|s@K?FWXZnB(=7LPa zT<|y#N4w4;ga+ diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml index 47566719f3..ae21500c8f 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml +++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml @@ -8,22 +8,80 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -72,6 +130,12 @@ + + + + + + @@ -173,6 +237,12 @@ + + + + + + @@ -415,6 +485,14 @@ + + + + + + + + diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz index 2f9588ccc61be8b50fac63248d6d03f64e05a719..693bb620f68837e788140f47b7e7ae5ea94705a4 100644 GIT binary patch delta 9652 zcmV;lB}>|?Nr_Bp{9o_XyYK(!)#t19;p6B3+|`>`pa1RdAOHAHtjW!PmHX*u_mCcc{roS7n-339 zf8Kp~is|7yx~A^))7|~!XZOMV^&Pox`t)1f)*F0HZ?=T_n(aQbHQ#-vYq9%G))LHr zUR!*N>94zor(f>_uBx@Zb&%!m5BKnU!Uf&oNY-X;Z#T5gLuxK0QAE{_t@3@$;ufh6%-xS&AVo#en1Y&Od$n^z>(n z-+lOh)8Ez0kJ}=&w zu4Ofj#tdXJ1G!ee!1$CaBntEMsP)Xdp+9ta#}Uis?*94i&jhad>C*>LKb>*olkOiM z(bD*gr)hoE0S%7is7o5^ zb=!ARgL3u5z(}*|$l$W*v>oj`+}zA-srv1T4K@4%H9{yY1kqd*DRoKo4Dv zU2jZps6lHr+>Y30F_xaW0owFsG%YfF0^t*SH;8{U?+_2V|k{)2V}h zJU&3`9_YvrCx$mUw5xveApV~Af1DbH}2sX zg!WkIK!4SDRkik1clGh<`Ez)BjQ5|B8(nqfnsh%K&6Nm%*#AJUK7L9qQj_kp)w>@Y zCmY{3x?T4%;bga(b(|PNI)gkdlC(O1H+J5rw}-HgXtric!(ER}$_6oQKamNL_NjC$ zK(6*@L$Gh(WJ`Do1fNK7I&(USSRL=_82&UKeJp)&^FFdk%}q_jey-7H2fq)ljid+@ zz2;2UB5aSP!xv|HNsF9kK}UuF8`&*g7{yLAFG(>kudShkaH@URu4hbtFSbvAjko2$ z8sVBth4Bz5IFDGT%Yl8IjHKKT+s}bcLyj{=e&sbhiv1=Be24-k8g}vEVbftE$c#Ev z%I4HCmD=`tw(^lqQC>D+nyl6o)L@Qn^T;(-yL}CO(IeX>?RHzqN0mA}%=1Rl-U_2g zWYEmEEqyQ2j~(uFWo&1E^2la?!;qja+J1ZSObmFy{%jo~GE?GV-VK9F^8c84%4~z zr6?U0xqbJCuJ(sA^{xOt6^4G0?a3VanlB!`om|q%2|X@GKaCuvc0IO#J=K%E9++&b z=bLt>v~xSdx_&y=WN2e)fz6}a@%^7;`%0th@k|!4Zb(IoFEtzVEo6HHHWoqqCUL|Z zj+(;N<{SRH`>sCk!3ROe{qTc(zJL7nA$@*&9GIxB{+@sL&*|U4r^k>EwA(eDO0lc* zAKg8gF2Su&0Lm%m|NNYPJ~exB`>pTe8`=}Q;e%jX|w9?GA zx>-ULJ-p!8Iy8rVx{*l_%cQGJpYAU$Rv-&d+_{E}lI^bG&1uDdrRT|%SuhKXU^A2E zrWIo@$e`=1*x`}G61sBt7q`cbeBy6Q_{4uyTl}s5T?WHnlHwwAuI&OrvOpGFs)Ls`kV4-sN8jGueAD=A zYrMZ>u#gLf|-u3m{)v$AB9TgzdqDw|K6BcvrJ|KM0;;LZab*$5m0zOx(OPV($J z-`OR1{d2v`mD~+iy-kZZS@kw8Z0$O;{NO9BCAs}FWBXEnMJE%dnBT^Ju7QlTJG!HN zrb1u!$ZDxY{gNZFg=FbJbvQ0(bJF(OCOvo#{>_TMS0m z=RS)TB(|Rq*S$i$uHDzty;he2yKkgE$?i`oGCVHyY0p=lz`JMHqf*VV>KB*bP1x?Z z6}{!k)t>Hu#s=0N)-XKz8p>U-iZ6YB8mP6~K{i%)ySt91i@VsK^k9{e`%qn8D{`@} z1E#%50R{F7_t^E^vd5jQh53&d!}o!mGLCNB0mk(~h}Nj+Uim*x5$iGT+#gWlx>w2h zYAOWluT6osr<(2m>D3*vo;F$N!G=MV@2d)S9ZNNTZ%>@osyR{+*b{z63FfeHBO0GI zVY4cX=h7S16f6*y!L;5VS z>hj+GFs|=8yiFCUm=s=VR-Pe7b6cf4zJ|o5szi|Nbx_AT|E(f0x z!558x-Xmr4=itA~%X2{le7-RI8vaw=_9-s=EO$NcS%=F9zSkYlW#PjGWv%{%Uf9`9 zT4G%ybYvRn#3Llbwdn`M&RJ-uG40vs@u+y(KwI-W!=LpZE2K5k8913`oAT-%smW>W zciz<|?E_Sz-}Ii{ zIH+IQPyLKW<@I3ws(;!l`yVY#+H-0TW>Z7E8PNTZdS=mGt1jL8!oh|vgdU)KWHdeF z(OqpcZ%tI!Q*^Ee9!j9QrxIR?%Vf#eesT0PX!aU3LmHf@jM`JZom@88C))Q=snMZ- zyJko7hhC@hG|K>_UT7&72^S(hIu$*4*IvgX?oPEIwCJ{)T$FuCG(6^m0{SE4K5z`Z zu}?dQ{^-YKsSe|~EQijdFUw5TZkK&O6pc;UkQ*4Ie?2Fh-MkSgCY@7H1T#8&X5Q?X zso9%wXnjdqj%{Roje}co)%RW7hvo%;NFDtgx{gvM1fw{jRgQdJ}U+jTh%9o3M zJsno$z}C`8uz#V0J{t624`}ZW?fNl!(wsI~%A)5;v^6W|Zo3RJcmq35%byi3zE?0Z zcdx#`GB(Ah3NUlpUwMD(^!$HFAB${>xAtE4o8qVJM=ZA){*sOG6RX8_r}1Qe*|*+S zi|doB#r0sCKG8v)B9z(+rA`v6$u&+m32YaQy?Tw@U=XG4`hba=;QqiiOR|^ozMSMq zujQXp&^R>W&c@jx26?&UgC@F=_#+efL#^-IPD-zkZnt~1z{p2ZvXQMz+PHzWX?7tbA#5&xa?E$85R)M1 zys29X=yU;22iTl)FnM8lrr^wZmNNBt*jEspUgbgWoltcQ=c!=;984b8ynH8Vd7Ry? zW7%GAy#sOigoKTx)oc@A=BaQX{;=Wrb1=Tq^UTq@pNW_#}FKH+rsLgyuC4sG~M_hlRJ7nf|Iv%A*_AD4|DmmR?0 zGV^ZM+H0Ovew&5f>DkLqTE2FC_htrvNr!&cpe7zpJN{;d!B;%|%{C-Ynw+<>XFK;5 zSxY>lIWg)BkMgp`Cl{3sfb;9bL=~xjLquOeEPmyBuQ#<;UujW)d|_|-b+4VTFl_!U zRW$LU!t-8T@C6csFT5bXLRBvJFzS zWd>7)G4t(cF0*B-7J6fU9X8WN60;QYH>km!JneCHDg0Rw#?q0u`!8Outx0QD{wqrURd$oJNWp`a5$ssfJ)>#y#*SVT|!H+2n!rikiXr7hN z`t^q{wC%0d!AZJ$|Gs4FpP%mTA3xVr?0HSx$CCB!hFX7E&E2objeCFhkEh4f?Lghf zl6KQ>2a5K8|Mm1Ct+)NkZ^jQWWDP^s?a#&-@`fSrcHjpL%U^fjuAjUY# zhNJ9ukUNf;)>u+;bb>kjd-rS1A8-5YRl{DjsnzytH70^?M9@Q>^l>o?q~4j$_Ugff z`;9m6UfQ%gWLn?CTQ1(Xhv#(P{HdDm$PE2|9Bj0IdyUuThpW2e@5^pqXDBdyvZiZx ze?N4m{E{aW!M2K^Em4}DJH_ry6*hg~-rWMh|`% zbgSy|A(!8DJovrF=hBb1FBPLW_=%A*CB2x^#iTiHB3{4?u6{pvl$|m1?G&;7e7{H@ z@$#;`F)Bn;UhRipU^opWaREwVXS=;M+<1ctKl|QbPpz4x_mgN3MSmj|7_s~JhZo$B z4aVHMiS4b<)D^9k>Fr!A>gK!2>yc~X)aY~_5ZHAa8)V_XZPi4-@|oOR?X9B$hS#kD zSEyJW)n=8|OM3UIIWwWqa6R&%YENrxh|LY%zoBn#Zd)FuQZ(RLy@ToZFr`ENRDWG} z4|z-OjzNEVF3}!I{RQVeLVoU(F%T1f&v$<&w9QYSJ^&3j&0z!`uERy;Qpa&EN9YeR#MwTnU z{6BCP>V5k3pS!I}%SHIIf4PT;r$6sLJjL|TZ*<_grW$U!esF(%*M8gcbNTjv+y2`Q z9Ju?<-{1DvO18QAK&xRhhEG*nJqNqF&U)9`O?_=s2Y}8QMYr3U@mc+9*1~&&@SBcR zP4lkvQIP2H%&ZZ!>pZUM&BVL_-X6}ywh!BoCB@Yb1{DN`wHgd60!~hrlw@n3vhDb5 z&wWtYCPxLoc4CUI5U}-o^7XKPxtv=A?A;CuhTwo0)R3=H!nC?p%vlrye+pMMOrr*l z;{La3fvBEr4}s8Pk7%yi?oW=;l$%YHElsnbx%a_x=Yy-#4?V4IY{1KOCgh<8^{g~&aBfnB$;5Lx(d zTWvxlK6l5b)=ak}V!32@pG@O8puvho*lr%#7F29**!~UMi-@4eaif;5aMJ6+$u=S~ z-3sNLt~uLDSiXtfrv|rjflqb&g6}(R$u>7c|Ay#ESSZTEtn`rm9&#%oXWjK!wop_z zs&UnIWLyoe%+YYu^wM*GJ5_t&Rex)~Pbg38ZaOQhjI9%~Pa$VpR#!mHoG92JkwdsY z&-MS@AeK!;e0&Of6xBH|*kY&sZfL9dAlB*-T?Iq#^5YjL4 z-%DOt|2QN*og>!{EF4NfhXz?znV|S|eUxl%K_^~mL2TVm!DVhFJ|8(NyovEM<|9N0~lN{BLsdKo`qHh z)7d(mbQXsI`NS>-7Hp{ZsN2uF*Ot4HRl6 zaqO5})ekk9W#daW%0Em^OF7L3-)vlC`}X$cHfdv1xhLB>+XL6e4$cbMwrs1M$~A@s z{{-(bZd2R)gXYvz;-;~x+2(#ZY_DtF3i}KcZCVSkHdDV8LDfco(A&Y)i-!9V99li6 zGnNKtC0{)@mcu37{GUF2{QRFm_shi`wzA}1rJ((S!o#cLODrfL&=etqM??nEOO?KFeW7RF=5>YqiZ8iB@HS$D!ddq z31c}C%z=!J0_1C>kO-5wPM9~D#!RU-%!5=igmPvYc3w&*ZH_Vt6?;;ZtU&?q^JzF|jY0`KUovO2I3Ej~+sD?K5aQo?d+w9+fJk}I*| zD|V%<5W)veNH84ou`H;-AfYh9neymhS{-cSgj-3op)@(^ljMo>EMsC>TkTsMEIQB> zJ+Tb>;f`l7Ow1t$u35^AV<6~2+dXuSPMBn+O%kFx?hMg9c}%?xA~l1cd_~!c(i2;I zr@5z85brX7Nz9NGd18V|!M*aV%q$iA=7wgijB*fPhQx(sI`hbbirmJObwk{)s990H zqH0Cui~2;3Y0Dm_V}j2xHbN=d@|dIL(sJ~Xy4xvX5H#sTQsP(@CW#P))+EUkGF9On zV=G2itjEo(m@So_`s@@eg@njmmPEi(gyyPtkD@jOiYIiwB0X!8aN^4J@&jdzDUFOOYE&|4$-f_9& zuvNa|Y{lt{lNEzinHAG3rUnRN`D&(E z3yDV)b+Cb`7#X~xqTFQT6x?l~@DR2V#{$(Wq3VazSvVD7nFfwFSteyBuAG__9|~wMrk4>91COCYvz?w_@0GQ2s?=k`O=s4v5{oQLkR^6W8z*bmNOiG zu%d}%QKA~f5WAip&MexjGJ`kE$vK-T@OjQg$!wzEIACd4(scV$SLTeetP~hU5kydc zFM_*}0}XQHgB2O25Ex0^J4xZWQb5cvYn40848u^oD-;wf6cimL!ZKk6O{i=Y0EbO9 zSWpu!CpaDLj_Q30+!OQi0`~ffJbbMwlOQCS4ORjTp6)4d}Y{w5muUN zXqecfbhbc_HU(ggfC!!#u~9Xwurf1vg=T(Q6IxYFK6w(A5jaeJbw8UUY<>Ysui2fYv#{Q&bEg z5>C8035VbIW*PsFgMh(Kj zt!V`dmT))@F|GzIf`CQJU$V0H@`FY;P70ihRx?{r4`L<-US?DwBQ?CZYD(Zwh}nnx zIj&SF=}O+JkuxDEAreQR4a7(!q{bA4UjaE1+SBM7?SKrUV;1sdg4Bm5i%1m#rGOCm z2Ab27{UQAWPywoY0UJ+$0+&)pj(k+9lo)U?ahy8FsO4sl)6eA;y)5BB=%B1|78p7p z^bnG@E_(p73);`+hg1&m79Qn#$3KBSRWBh~IB_;Xo0tSfHD=DL8+&dUG%YlbACSLqu6Br2{-HX}Jd2CL3%|={V$nJy(QGJVCI<>f!;W zs|0l%7Ho);UJ74vH!V%erUjLY$pJvigGFW)1oIO9lp?Vbm~>AWb;LDtpik*kdMzl6 z=SfJ7lm{RIVgTinT&$2A8IZ`cDhn%soh&X3g$RI1Qb0La6~JIr(u6!C6-ce)P_FTk zK7c?9J|$~Kqr|{}Gy)qzqQT%`6^~`tlChq2964I1nLDNe2f&RCxx9tbKsKxlPn-ON zBG2d|WrGBY8S52Qf??SK&nE^f&JB=KYUZ0ke`TX)kb(o)Hmtaa4AarbuXL7yS%SnM zO6400=u^Z-`bSItH%Lhru0dpr=DbWZ@}_7I)qQ}2WsNLC73I6{Ny+4&gVF0sI38 z7#4+Pf%pJr>5YNYlOa3F%04Fa%`63!D*2UHgOp*+2;j6BG$IQvp#{k{6=gHCY<_|T zTr({}6Xs2SL1LJ>((vpSSPACHoI#)@Rv17inUw`#ZJ3*7m;?C=M?`|rCT;*79lVZb z7I`fNt}~T6R&EEpyqy04Og0vop%sd8_%~lXii`;7n&g1QTr?t>B}GWyP^*Na$h%A+ z%sav|P>@g10rRtd17;$Yq}!$} zxOB;xm}Mkz!sTRxO19`Ua9W_ei3qF4Gx**VbE*d$95%tL1mz!TZO2?*5Gysz(UKek zvQ?pfNK!s}%Q?Q6gM%uFSX2TG)N8{D{wQ7!mV~C(WCvs6$a8fo^HF9m_H4fl3CNAM60?-9>jek&!`UmD2BDj;t2!KKh zltL^=!iYqxq*=BRVNw5}G|}*fKt>je0&zcoX=ULqpbEo1CyfY;P6W(AifjrpFZ-`$ z-xpAiCmoQJ3sJWnG36tRhDd(^nsY()60?<};Vb1_?47Y%&ZH3E! z!2V1+ScK2fX(X|(x+t}%la#Jtby;#`CxZ6@X)6+C31=09YmWF1k5cDBVj5&lA^?+k zFOkI%WG6Hu>oZiku-WEl@1|&RDifm_U=B^%<;WnsjF?md);@ES!^p19>3q1&NKP&F z0Jyg7a*|3OosX6flPHgtT4{7NxfIqRB_fSZ?OTvEQMfzr6qSfY ztmH^3Dd&`ufWb*uNey`mlIjwF)ToNKR7+(hNR*70l18DjNzM5@qS6=kP25;xvJuRc z%`c}Zk=6+Bs4!M}(g-P93|iA+hZdo4zP*5n%L_FIrx zCC)<<5_t|4nFbSpvNg#L$tZKSf`0QRylLdt5e{5txFeb5lD9gCKY<8t4XKjqx1?K& zb!8>eSz#Emmr@O6tkmULm2od?N@w1L|1XEG8qrhoz=BSRld>J;h43;)mQv%e=7;}f zz?5;GL_w0xmW1pxq|O$9DWQxYBAfFvJKqm1A|%1oGMXaSS`ub6f)jC`aiD-uO0&zH z+xgIW!8zyDXUmep%$LJEOs}&%3wSPC4%VtywQs`zmlA1~07z+6S__jQqVn4N6g(rU zR^Hn;vEq{r#YcGnQ|G+PJQ<@BBSgxikULdL?EGq>#%A%7gU=cNv$OB2r_fk<`PM7VMTj~b0 zYoiMmZV4D!SV6NRa8gLtk;6Bq(nP&I!HFyd#Y#AxAgBcd#9y6@V+CkQ&9e(czdgaT zO2GnKkqGlOIaq^#b+5}q3EpQ<8&fGyT|f|4PV^Tu+DxsJlymK*E%`Bvz#fUPY>W<2 zYEzLQ8cAsRTuOz>+fii%#+On$WPSiq&Io~3sFRK%T4}e>+{m{(01rb=))UPUL0i?XsQqodEH{1d6vL8K`N!2tc#V$ zo=T0`qA}MZ_U8h%h*6Be%>;qOMH=FCDB!C;I6SWrmjG(zk+Xmgh#fv30#O^li^#0vz!xefV0lvZMv&~`U-?^qo_^N46xHZb$j)<)l2Vwhvoec5W z&8DY+wIWJ~GA%|pm2A=;qZbA%AR{BF^w1x+!-Skqw}jPP9>OJ_1m?;k-U>c2I0nxc zQk7FSj}$Q2D3%y&id`6Nl?ih?N2_BNK!AZ|%N@Q^Ql4ZM;AjD$8;)YfM)H@lioolX zC}q5-#pPS4%MN2Ir(s4mHYw3p%JcXL?xRS5hDQ$#0%TJuY*b(*eZokqF~Urk57ZxBKA(mfx(j8MKg(PtQm_%M4%B;%~F6kn?kTGBtM9_v|1RX76z6~4@7*oe| z4fpV-qrA%e>C&cnDck2;Yply(v{l8ef`$SOg?8m}!SWoWEEb1$QePoLV9?SC4KHGU zO(H8Pnv`VkVJ%k<&+b{SsTI>87KT|^2L z1tD04-Uuvw*k1_M+6=!8uYj0knb!uv7~1ryuMJS=DbE^fl;f#ASFU;Q%`% zW$-g82a{!{zz@I_#*~`>$`dpI)h@$?^#1{#XKcfL3IPD?>Y0iF delta 9331 zcmV-(B#hgMOsh$MABzY8000000RQcMS#Kn_vgW&fh2K15!vObXU=JV|5K6$z@x#5S z$0Km{kw-1{k=o1o_w$iiTdtL*s#L3ue&|+JCK(Y71|z;8BeVX;ci+7H%Y95Q-~5rD zU+$kC|JOI_oA3VT)u(^E`^P`N6>D;H<$nChJ*3B9KmE&pq3y%N)1P-Ao??3VmaeJ$ z^mKRs_{n{6e|<}?n?C(kxAg{J)0-_}zGl16Y|VF{>00bQleGl%pVk)NV*2au;px}= zfU9b)ZyjX0`@=o_o^U~TIFhwl+uIFodsD=^^H0A&#+Tv7*Bf@5546z#$^Cryf76Gj z=l_71y18|Kk57+}zdt5=|nfo<;y1S3{3*US>)=mtzyA1XAq~ShPc8!7k^KUk=e{KghJp1lLHKMz! zfun6etdQz+pmIQ;RNnpr>qFzib=y8Sw_&!=>E-Ev;g9q!Z4GK`+wIvX%LZ)zm7edb z8a6{#fx3ME=pHbD@^w#?w1|HBGh0WwjLn=R@ZK9vx!+;WLdQG{IdH$ExZkeHOikum zR^w>QKo&EQYxN6^Pq{*(Fh7r4&%7J@Lzj0Pv25<{U+(@);F_PFKY;q_j2oYH|M-}m z-DCQHbIm(_j#C&}4~R5PD@sZ;N=i`qu6}EeX^25tWss}idQhCE^-%{jIFh3-X{gt2 z-$@P1)ei$B&8j1V%c9eEwC`|pGq0uUw<|W(@C(!kp|lW0b4{$2R8jfwPqza-bTM|l zF}FMJ)px~bG-Q%Z*#NA8!bw_4c zOV6pG+_dGeQHuLvJK*j09n(NMw+2}4CEn7T>i*+T6SuE%JGA;wD1i>hLf!MJgFHTy z`~n$&$^G~9@9C=jwJhAN89rWsky0%*v~ck?BMsowUHEIqSu`1T7>Pfbok;dFKLnUEa=D(U?aPw z3!~U+<~1qi<+U}G5Kgu4+Vza-@5T11@wWU|BV2Q-FdhO0=Mn34Ik1nDk(B#>`#I2m zX~=P=$Zx!cN3q}JfDcjNM8hr~JZw5l1esBXO4*zmrc&Ep&sILtDay+ROq11`f*Q=R zZ63L%YPYX}FM4FVq}^^S`KVHdhk4#e+FM~1i42>;{)4+m(-}*kj zp*^uX&RVx6u;?6Z(lx%keZ%!*NJx`|0f>~e$o0&8>tr&Ab23=pp4v!p`(3QJ?zqmb?O#@t9 z!Y1$cPVthY2SUVGZGZXNUYiB9y*A5e8~$n;ZNG&tEV$#h;uC*c!YBTt+Tw5Z?=l$v zk`xz_b8Qz0k_EEZQYpNwffV|7Ir{eI=BvivTI2m4gN0l;B}@2lN)~eBlq}@MyPGVF zsk?*=N|rMoN~-Z(It^-nCE~jxs7qSS#myxwq2(nuy4G?e@0CkzboENanw2G++*%G> zRoQ&n93d?+`3J`$19u+i$VT80@SWZGc9Lh;`OYr6>!0gguHTO!Q$*Q+$VQbf! zm{(H-qG75b(}R!c4F*BpU=EhJ0-sl#zOo0GP; zHtE50@UK?%)rwwWMYkvUtx;!qyoO+IF=CriIrmw#AhG?dxb79|b?v^E?zOrM*nK1Q zNp^oyk>PQnPkX-d1l~Qn9+hf_Rlm9fZ^CxRt>`^huJ&{{Hn8@vhT+MVQ0{tFeCf;6 zK&{;lvazz;-E}N~UEIa?qz9{%+=uG&T9J!&9Wd=h3MjBwxW}&NmObudEzEzw7`_Ya zlyP+14lu3{LbOIj_saiaidc_v=l*~a*S$*4H&Y>4e`yN5J=JXgPp|HX^|Z-C4>k;{ zd|y?t>sYFJd*ZZK&5?q@p71kDFo%U3(fF(hn^j>v&n~NfNxj~jhOBt+zh;YYf{A@q z_!}#{SHpc&{Oc1J*>SHsOaF9i|BFs>8`5WqRhRefhjD$+;eD#0*1;{PfF1oofsQ;j zKnJ2k=)Ugbq?ph(@EI|7_>BXY*To~)a5?yl2)=0a9x01I2mf7Oo(m%2^M%>h@Sp0o zPjT62x$Aj<&pKQ_@V)JTE(;$nC~Ng6^uo?=(h}WjS;veOYFzcDwBR zp=fN%hTOmy{p&g5?B<~xYaHBytG@5rJ~S^t z>geYfm%S70uk;=d%>4x!Eah$cVh`+6zFzEq>*=r}2ey_*g8eHU^wFUIc0hY~XxER) zljgL^QWiZ&qODmuciUxJ-Lr|17e`dDO3 zytVhT-xNP(KVrGf@YigFpI9xfJB=sHzV)_RT%S}et_Rcfi4N)%q109=b&^m`u5rSD zNnpEZ?9FTB27@SV*9T101osEFS(3es_w^)CdM*E)g2tf{cQ(!rG05vBA2iX0#2=Z+ z?`wVEc2atUbi3W71x7xSl8tO#(#8#}O|v_Bad}3!JkKC%#uLvGKs;v`>cW5vTM@pk`iXT`I2@D`GAbPw=@{F zgPt?BKXO)k8qhgQhAFUf4qL$qUOf1!vBGvy`dF z!@hv%^d=8_?}VyjI8O}&;9&Bw=Jh*C%j4{B9n1D|>m7*8CnRhnt!A6}GEapA@rMn^ zpM&v@o@b8M{Y=D^$-1BY`QD{YQ9FbO{q^Lj=`wRUecn2AF8e-u;H-5a`G;+pw7~l9;8C zzd;S=>~StqaXFLwRLQ|S5{p$+&SO7WRxo!8zE(=^C7dcPm}?QoiwHiWSN8N zcHHPIUWIskZ(~i_An^{auD>le^1^#|(tFJ9nu_w0@oE@lJ|h0>yvUobsa-SDUQ(yL z$h#R;yVaR8t{K~^qCLHXue$FnprXF>G<4)m?`r>Y_xi;Qu90qkyRE#tu^rRl*sI<9 zExYRiNe-Ezx6Yy{z0TF#D}GF25bmCBLG!G9)~`Qwp>1!q4o=e5&p(%J{nOLk{o|*a zioL9f`&hER-B9ZftGW9%xp6<={p0B|bvsb^v83I!+kv9}e?5Ij>utaCoACn-S;LTZ z`?E2IykW?@9ryu%!}8bNH!OP`MZ-~a35YR{vf(JZ9psK9rZtvS9Gzee|K9x?^T*ph zd)2U4ZECgsT8)XI8xizSCw*Lu0;zXqv%Pw7;eO-IyO%aC51H1t@Ro}=?%^ffH-D<8 zJ2FH69|s%lUgNd-;i@kA`?A~D843)atm&HF-w)j>zvKyjMX;?RXiJo)=T5OZQ-w`m zb*5*{*J>>fr)SNJRBJIZHRzzrPvq^VX4heKS|BmU{ley_ofS6S0)Z7?{anjwQIv)I9<4fsB+n0(_9Q?${ zn37&i>0;8HHW9Dj1y{eHJIc-&`F4ufe!gENk9d7o-WV04DX;d!FEE^jlDGgRv9sOY z8g9J7pM7tzr`Al;&%^$&`iw#U$I)K|x{pVq>!U=Id=E2!B^4O4`=1XlxE~sfxpfoU zTb-#ZS}oJtxmMK8cazs6*TkvO={g{=>ozvX!hhSUiGJlXxw+a~M*|G6TLZ38u{x^F zDyx_D?o)GSLZRV$iQZ>|zV{~|F6l_ZldzTquy>Q1S7D@dD&;tsC zj-lIVBg++F{vWst^*%lS=WeUgauL4lU+&@I>Cd}=4^J^Y^cx+xuBnDwt{>cA-?rcO z{8GOCw*R&R2kw6J_qYAEl5K82&}!I>;ZxOC&%ti4v)*-fQ(xQE0ibh6(e1Wod{)1j zweX%G{H9}7)4c0^6eK!4Gi$``I*)65GchlKw}*4F?ZY-?NpbaqK?Q+ftpMt8^oJKoDGQMWwFhs(CFn_?M86lGKLQi(CVe*;WhsZ9uVB(rR+|us&)xB#w%BRE8`^3_|RN1J~yuWi`n-`(s3~45sG2R00!5~ z2!UUQXQ7qBbhb_>oy8$QKC#QeXisJK^UwWEsX-bwnr~m2-MU#Oc;gt0t^W6uC=(R{ zPm?|q8&;Z-vB^T`$EGr-0sftBD)+tnEA)1%>a}T8KvKJz-zk%*;B?=vL3A5Uy|j;c z2JMZ_VN#H6kI7k+c{?bKoFhyFJ1;5B^;@p{-l@*aUZYzwgW=)TldlsWe-ejY&)R$F z`^SUy6YKQ;=liW9*zVwLxI^c3x?H1mP8ulGO5)ftxvC#(GRwx7Y?ObPnwD~!4Zhj9 z#`f*)&27@grgBfVbG8SrjUAj7vTfN`IhAV+3;qe-W89{;_Xo|Xr^HQTRkO|ga@bzi zxE1ypDB83ZU~Q&;DT1nvf1tO6s}~LTBRI5rPG>9)&Pu*|Y%GUMxcNVQ`1t8RgYK7$ zIc#OgOJB+MR4-P${;~zFM?6&J(0tynwq~^BY;R|?z4~-@rK}Lb2Tn*ZoW{(upaQGV z`Xo40{u{kgE4dOYzG5r7B3Cp;Pb^EqaL2P3Cgu`tKlzGh2a%nl5OSPhAMbQr* z|LTi#_3Yn_#4WlbYR@8PodKI&!(o>(EQdW}?xyzCWE4|QM z)sAequg#oWO%2H)e}b_I7aXBl36p8`D%ZYzw7Yb~%iwgRESVsU)y_Lhml8Km?CT&=jAMa>aOxy&qh=kZrk6O6;Ge=8SZSS}Q5f~^Ey39{mL z#m!vGi4a2!H^#y~gh}2*eMA(}hA~y;6#SLMqlr4$KvaxOQ=up~**FzN3>0g{R^nnM z)Jn+u;dB;G1z4t`UL?z;j4VIoQ;y%M89#2f6}a^?)Igw=#sLm6c|MjL{Jod zmAjAw4RYffr5&XZ7)jhaN#Rjah|ZQZ#GPe^VJO}e3W^pAii{FrnJ~l^t+G{_a+_$z zH)kOpJc=Wgh*&AUQf!ir)jm2(4b-O)Dr`V#&@751MHZ$GN2!&PN9ZUmmE+bME?r21 zYM!-Ke{h$Xgv2u9nOJGQ(rl$^%lB%sQW&XODP5*`SYwiCxHN9zaAFA7+GvddFCL-E z=!#3H1g(iYnYI%$D9CE4U=idfv{=M<-XxwS8>4OX%BYo*DYXU2SnDyh>faYB`(6sIzW~zGi+2Ee}RdhJYMgFztTNrp9$c?Qt& zB{E^WB8q~#*hR-!Y@^^AEPAa?vW8_A9gIad?o)9$_M#*7TuTPGlqBZ>HBm8yE;!fX ze=r;+1twa3Nrs$Dm4yxjE|D?@Wg=23lX;Ml6CMgfwX⁢|sEt8mI~w3m(jgl&meF zg)1VYN+ilUPI-B@4yZDFo3l=i(EzUk@D8*Q7(-YHtb`A8Q469L<{DI>z>YyUxHYX{ z!4eL~aRBzpu|R&ZvUX+7<;P4|Bn4$ff2)}-U<4tP0>(0`Bxi;fPfZEj3DNr~Jjas? zC7p{7LkWnD6oEJb1Rz8rV=|@y?~0Qtv8T~B+5xad$1LQ_1Q`iU7J(`P;Q+Yt4PvG> zS)v6$P)c6G#*@IM)R9Y%0i?tLM~Op@&KR}a?BVmdoT8T{`Uf49HO>Os21Fi0f3nul zpOsxKeJ(#_aBv|x0_0d%vRY(RSwnru?yOFE09c>P(qUP76R1Iq^AQL>XUv#M%25P5 zt)@`++3L-~5KLmu$kz~Lsgw@ruw=^`7?^AzH>Kl9^jr}#@dU9JtBVJit`gL7Sg;{V zdMSK`!?ZLlIX)GO$pJjegGIs^aZtL$qG zQgFb)hLxq8F{K)5kIphMOMus-RKB5rK1FO~OYrC;lyu=5M7ES!Ueu3tCK?1=AK>^{ zBMUG8N_RU!iKZkGN2J$SSwMM+U?jqoWroi_@rDvC9C2%!l2Cwf!Ub=TGV%x|c@7f= zy3(05E-QA#lpdmDWGVOue-4;%iWx8YVV|<}#=sfLkey_jrvez6r9e0(?eS`mGK>s? zl@>#T$EU^RBR8c;PHC|?q^FdZ{W-LO*-?-fX09|mt_6fiiZf>rz=#zF$VO&mfg>B{ zdKu;bq{0!AV6=%FAUX$c;F(3bNddP^WsViq0Tr+3KY(71MZ#u483H~U+6HJGu)@DOZ zaapcPz}`R=vW(nh0tkZ4+5!%EfD>Yo5OPgeGbdtERdBc^f2A~1VB{MPpfM&c;Uxml z1#^vmP>cEp<{2WmlR)Y~hf)NKSdK&v2~bIYY$L*={y}M?;SYg~EEWage$vXqT|gCv zdrle=7M%!~ffU&k#9X#T%XTcF9#1+TR~Dk~2FOKSRM~vt0O>Xnu7c$O;71rDah-bO z8y964HAa!)eY~)5PExvp)n&~X_q5|@G@dj z4OsikO%5ZwDW~({HY1g_)C<5$oeW0;RJQS*OvYLor}k1#=LQUqNG%a4jqylZHNquQ zSO9!@ZE3=hos?HFw3ujQX9!6-AkVZZB%=_g4Zyu^HWKC}$)|Hh;zmtM*)W7hX6eTz7D&MF%Yxl0YCy@EKvj3Sx9dW0_#C5zxg8$X^N<};tH!@*?4A={9f)WbR%@E@o;!WFGo^gwJZD5#E{5+atIdi09J6SyiLC1e@1=6@>ot%$)oep5@HhN(NZgojwTD` zFa$#yotpO`X`*m<-YF^(i&)8#Qc}(-B>{tzZX~tuK~i0U8dcGj;-bt1iIRan!jQ@) zHOJ=Ee&%J5me!bT1aoEc%V|oaHNrb2+E#he_@?>#Ttr9_NKnb@;7Ev`kiZNR+y_NO zf6iF=WzG$I4|6URJiQNrSyj%RwGx2o2>o#UN<>$!)5!NAsVk=~s+4pv#&|h$D3xJE zB9+LL!{39%Dsdi?kjQhW$TXM$l&wj2NJg2n74(~T;Y}mAj&R^I!yU;a zm%P z&KbcpI2nMToJ+9T?BJXFYI97m`)Rg)Y_5K9UDg_H{MIy}C^p`T)Os$iY zbM2%p`7w(?Nr|v*j1Ew0m4xy}5?Vf&3SRquR2hNsrIZetA3&5dLSPl@f23oGR@%)Y zDpb7R0eBc{vYu$>0jh}996m!LOzmC{Yt#mZAcrN(U0m}|KNyeiLC1$=sqyv^wEE*-s zMv_DaEkvo&%b6lFe^+|27(wUJQzR0JQ3=nJPZB;`3#CG2wKUS!@xexB)6-fJr9%MR zHNvT6llB}MYpTV-Q zFj!Nf!bJI~Pv>ZL%mTPAuxz=*H%iLmx&j<6pl`#G@7PH8e|lCCD4P