From 149c9bd9274339312040b391cdcf5c2c0cd54862 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Sun, 23 Sep 2018 19:26:03 +0200
Subject: [PATCH] update some obsolete sessions

---
 examples/binomial_heap/why3session.xml        |   4 ++--
 examples/binomial_heap/why3shapes.gz          | Bin 4493 -> 4481 bytes
 .../coincidence_count_list/why3session.xml    |   6 +++---
 examples/coincidence_count_list/why3shapes.gz | Bin 564 -> 539 bytes
 examples/gcd/why3session.xml                  |   4 ++--
 examples/gcd/why3shapes.gz                    | Bin 1804 -> 1789 bytes
 examples/gcd_vc_sp/why3session.xml            |   4 ++--
 examples/gcd_vc_sp/why3shapes.gz              | Bin 1685 -> 1672 bytes
 examples/prover/ISet/why3session.xml          |   4 ++--
 examples/prover/ISet/why3shapes.gz            | Bin 1812 -> 1791 bytes
 .../why3shapes.gz                             | Bin 6536 -> 6524 bytes
 .../why3session.xml                           |   2 +-
 .../vstte12_tree_reconstruction/why3shapes.gz | Bin 3458 -> 3442 bytes
 13 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/examples/binomial_heap/why3session.xml b/examples/binomial_heap/why3session.xml
index a52440e5a..3fbebf884 100644
--- a/examples/binomial_heap/why3session.xml
+++ b/examples/binomial_heap/why3session.xml
@@ -179,7 +179,7 @@
  <goal name="VC merge" expl="VC for merge" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC merge.0" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="38"/></proof>
   </goal>
   <goal name="VC merge.1" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="60"/></proof>
@@ -194,7 +194,7 @@
   <proof prover="1"><result status="valid" time="0.01" steps="74"/></proof>
   </goal>
   <goal name="VC merge.5" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="41"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
   </goal>
   <goal name="VC merge.6" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz
index c1adf123bf2c5cfc8e3a7c5c9f3d5bb3a615622a..65e0441946adfe835e73075fea834b5c6f5fd9d1 100644
GIT binary patch
delta 4477
zcmeBGZdB%y@8)0tgZ~pn_3Ni*z1+BLHD6Ov;;~~lJne#}ELKV1%DggkQ)5%_%%n@6
z4SwR!S9cec*MBVdZ2$A|+q-Yy=Kec)|IW18^|61x&Ry?+Ua9Nyzl%?QP3*V7SL5~l
z=QkdkKUv0cZV&DM|9$k)?)m!X>(h7a$x^;I_hrxO^3}6n^Um75>Vo{=@8<K(^v~2A
zt7N*>mzMu7u$zDN>5s3WFBA4yH(TsZJP|HeRK?YoDs!9vVUGKa`14tAMYVs`9Lfw6
zw!}p)U+ft%#qiS3M|)Lf>i=2(=i|S3?>;`%IrnMHor4v}{U83~&6I5NyEs*)$6Ud&
zTF_RMF-+;u(W~4Ccv$}b*$`~s7M7gBW?HDRzW)A;l-8n*8n)$oeNSr4cGB^%i+ud>
z(Ek~K{rM*^xwlU?kmvj~?t=wAVl$?m44ZwzW>N7er$r)@3d}6iKDsur>6I(5<Xw>Z
zB-5Jb^_>3v=iGbp_Jm1AUI|?MVTOU1uxR5Yy@de>+*A&8SK6M<Qr6mfJ%7p8ds2<t
zQUn)oI%=6&Z|oK%a--lcW6T`Rnl{DC1KVR3%2zx-neKb_kWseZ$CgE#6?#P$GDI32
ztPEHxSU7+Gli%!N&3T`C1Wr!)u#d&Sk3-bh<5Gr}b=w)6%HRFFf8N?}lY8&P%<jCf
zBp=5XhHD}xPI`(mCY4;X5Ox0eF!NBk@WL2Vy}8|+Pet)|gw?Yj4hu6eX8LIv;2-#_
zWe0QHfkUCQWSM4fn(#&@RZn8kM9#SxazFKs9aKF3@5k=)H^+XwTo9uze`D{#(|<Py
zrtOViD_6mqP_*u`eZ)Zt`MKW`UKaf|wf*~*k@0$d#MQvYa<#^<mnJ9fpP{S0kRkEp
z>u$CEjPqk8!*@%@&prBOe*MB{OO_bvMaKUSnxu7d67Nk<p}@@2!mrr}zS-4RtoZ%@
z$}4Nz+U1sfbHe0rK2^4webs&1QS*Q1dmjtFNiuPruv8?NBlm+$c-K~mo<lzSz1*zd
zUcdKTVyW(>#B+VU9uq_7tvREltj?*ev!%#gTgN2v;f#HWvER>SYU}Tue*IQjy-{P@
z?<Wde59WxuHEzs#r?ELy=%~+wP?5VKdvpKiFX}L8R#Qt@66F8?te4~YH4DPeM6#L)
zTs%Ab@$=lOTbIR^TGgZ*$`s2h&OcguVFTmBvW4F+?8>YVj4?<zJI1v>ZfBY5(Z&V~
z(V40$3unhi#&30bD9*WZ(IH9Av*GM>PKwtvUon<2j=yQ^aKS%IzFK*r<)PLWbNF4w
z&sE2qiEDAWwsUJ`$Z6?+=M@|G3bAYPeVH-$#2luq(_FqQ_Ocz9n!D*v#ZqPoYyJ|0
zXIms2W;1SnW#oD-JGUlqBG2aFIUWo%QVYCh1u1PaFk#u;KmYUdS&V!)mEyz8i}s!p
z_*vGaQE%fj_p61^{FU;{etg@+XOM2qx1qW19J7!2?y!wcTM|rFLz09m61a?$<SUO%
z*ikfzPxzt2`8-$44}YJs+{|Uzz5JnEz|EzuGjblPoVz(kBjZzxYL(b3mBmRL3op*_
z|M{)`xcu^(i}p2pcKiRVoA6xv(2Qh*HAR-f6Q7lEX?n`mZ%I8azVPzQ<qOwbNt1K?
zYw*hWvRRr>=X1lXx%|zJk9`=5=6q3{n&85F*Hc8*`P&bne`SFk2VOklp5@Uw^NNyE
zbZ2_0$h{dW_#2Y=Mf!hCh>n}@*R0AuRf8kvn`632Q*rz`t==cAT4HLnj&0aJvmkJ_
zf_9>JWB27BGrL}%jj#W~JLl|EVf`ylc^tp%o6R!!IT7qvw=j2Ip6cv-PP1z#nMtp{
zC?jaTN07Ue;qPkON`J2yhYJ^rj<HMJaGCPt^n<-dahfwPD}2;X-W#Q#;JI>twfVH;
zOLqt~s&fXaoj#)>JF!$X&2Me9#N@rt9efT|<(<f^@_%ca>!71rm?r(bzUi#Ot0Sco
zi_Kmn34Kml5vF=}xzU{d$^PpM9=};QJ?!ue=auWDV(zvy`5k&A&wgpez8x`{*6WVj
zvIfmR8x$zhR}icg^40XtoqM(WKF+t}+j!ZG@x{_*KQ0B$z7_G(bkDE&2(6Z?)m87S
z!sOFZAN_f^<zVR5yx%Eq_UHPe9zPDKFWK9Ah|lNOf)c?c!4vPPC2v0KIQvOghf;I4
z@l^Z&Uw+)b-#@W=|7?~BRm-2h_@_QL-x|3v;IxbD@+E7Xdt*G(7Eck_QF1d+&W=yu
z`nvb>-I_oD@A{wq?oDychIbY}v;V(rR1ev}nfNSftH;tsW%pQD>lR-16ER3U(IoXq
z{?p_7<LAw{@0O^$8DZ^PyEf55e6Rj-^;Nt}_UpD>IeBXSkB^gt;<x|1p&?hjlYhU$
zy4%6#j%)udX+EuACHUd3k5vDh4(78n-}7)@Vd@H7@Z;>+qV*DC<%c~>{>q(y_t#4C
zPn7VXQ)jh4Zn*t!zKCh;JR9wf;P#VWXUM3}WmY?U^O#`$vYnAC(+sMA)vZ;V?p?P~
zlu=zg<{aDXM;AU{m{&V*y4PZ@UytT*|9*Amj}Myhe@e=We@B=-{3iK8Q}WwfOT#k<
zH1kgCO}gyo)+XokQ9S<7-`@STdps<SrnT?M?|h{u{K|DxNcZ7hN#ld-TpsRP)7ff#
zL@{tS_q;%z#g_ha*FLV_@rfsWo~{$eakcoQ-0-xeJ9e>6o#MyVv-8JGyW_iWmwc`$
zF1M~-7B9-ab3xmhxvJ_)u8h~X{Ep^ug)GwRRR8_3Fmd6mmRGr9YmJ0W#dd}#pSyQ+
zg(R;x@4hOQq$-6!KbFnUf0Li{cZ%@u@7|TAcIR0Y|FXT~-JQ0{<;8_#QuUdO!%v7x
z2<*<)+3>LL0fYbl%%BM?)?O3Js$Q*UxPjg2T*O83*ENP8J-B99y}5oO^;g5(rE{Mu
z&5n8FrMGE%_nW7Ou7>};lKUj7j(;c1=}84~sZ-u;^18%v<SNIDCnh@u`qup3;rV+G
zV^jHyrM+59J3759JR_eza?o~MC?oN}tbW%jwaT1}Q=>|b+U>d|61#iacjK1GsWDg7
zj?W6UR_;8l8N4Zc(&-s1KF4XB9sTou4u_4iR(izAg&hvZmK;zm;=9ST{52c5(%H4_
z^Dj-<uy&W!jxAG;{T6&0ajb{=Sg3Pf(7$i*O*ihJqh1}DceDOjy}7nZT64-Je_Lh4
z^sCAj>t!eL|GRv)q5NI{{@EIm|1b8n?F{{WH|@clwJ(ice~gV?|7MriZ=K4RDKmmT
zIR5*sVSByB;Bt<CyUFe3us1d*vrj#rl%O;3mW#t;iESe5Ip_Uioa5}R_q+AHn%ILY
zW|gwM+B>(;d3r_d@L}hD@>_m(So~xuoO{xL>+Cs7Kh~>;)ZYkVdj24?fb*fztV4PS
zi>H*Sx~_b4UezZn=+RZ56OU*9*#CG{MWBht!x%O}Zp$fp8jm)eJejb>x?uU^@6M9H
zs(x_9v_;CU6_-%W7IAMqRJnHJ9Fv4^MQ4voB}CiQPVG4<VsSvQ!dpX;%|LK-sNqy0
z=duEk_XW}1`?L76J$>tEO*(z4_`p}0s=0h($(QDAsowpp;F$Aj*H8c5|19FuYtZ+L
zerOvWA2YS!Y?9DIKcl?OzvHE@eo<THdvnFC#kVA$r~kSd7;^Y=K!df^ypF89Qb+QG
z>YSw}pIY-h#d6^TgT$Rbo_^|3+2EMta&<ZLa{Db0Oe#8OhCDjtXwB-HrdjWLu8*fG
z`LAEWeuJ-8f88SYZ@cn(`w1(qqeatV)`<1YauMJQF3?IySiEhOcS*R>g3o()++KRo
z#8hE=;q9m8Y6ecP10Owo#QeMe%Cp6p*JsUPT@%H$m&wS!DvGU0mD%#wwXmnWN|NP5
z>lSX9{alB+SKwO566RwaV$N%CrJVBes=s{Xi{<_Q6Uv)jRW2-!j+(B#_xV(rU9s&J
zhI{TDzP@quKI!7kVHeh2sJFI#@%fF}v9DfSwvv;l&B|*{|Ko8^_we?&jk)4gOxN%6
zC-}Ck<Ehv$a4*WYL0aVSzDChLHKTnNM;5-yI`3oi;P=*pD>^6X<{58E3ExqAcj1OZ
zYo+UV)t|jSZ$DSsp|xf^e3chUzTPBKTxlBS)1Mn8|9s}0WiFrI=*@F}S0Z`+R8Q<O
zgDu6^-BcqVU#nYfC-|1@&5}N$u!!l)6VlDz8kNMQPuShNJg9VS`pvb+KHk`$d;Hb5
z=42hiFef(iH`5bZo^^0tmi{BQ?rr9cL#Bm~V-A}1C}&)+-}&zJ&x?%b^Ocr6ovT{3
zpw;ADM~@$qySA*6<D&ViH@vwt@!lr;HAb>4P2OGFy|HvRr=msas(ov$c+dX)lD979
zxub)?J;~&?%JUty66D1fP1__>Hh;h5Rsk;s_N5BxVYj?A1d7$P4J`y6-xcMXRo4D`
zmXdwy=<Y`hikaaI%~$JPjy8DS>MqfElKJ#|=!N`}PjjvtF?+2zBf4X$!^OgcCo)Va
zHbTFvPQTPnWHI%3H0a7KUzBpbN}ubw^C_{Suod&oBdbnre$dA`r{ZQ<*8gphPK_sA
z%R5Xn*>Yo?{MCx)s)-(a=yd7Y$C_$Ar6i4%?gBQEs-t|?%Ty+p+EpdjUz)g1_x7!L
zS!>k=-&t04t$jV!ib<&IwMbfn&ZUb>F1-BunKkeihvqH~-!eVU)|f9^^OV-l`SK`Z
z)~~n!*UvlnXm6LA$kL=G3cA@#&bWHNzPax}NBkqLUoIZ`pB28>NPYObUDP>D>gHMH
zbT&89iJFBX%1>hjX8H#2HL?G3EoVo)OhDHWuB^?%5nQcIH#Pia4mJHc+IiUg+40QD
zU1tt9b{I`AXf)<=EtTHYmD7KI*VOB0BDOe6OE!eeRXY>O7HA>SpmkJAOaHU>`kBtj
zBD;C?x2}Ghv_<K~p@){K{&OO8ZPUZw?Ob;&_%<7t_~*}!4c{ELcdz7+D6cnhdh_-5
z<a(Z43Ou({i@YKfWt%h{92*X&OsOafJTmuRz#=X&O^xX7pCct}`9dojob^)=1&Ck!
z{w;s|X})@cnJaU+3TDQixKbK;ZgMD7zsI3p8kg--C0`bV7SwwcoakJ#@l-ocpm?_B
z?4!H1WxY4B1!;XN(0uXzRYBhGQ@NAZMoZ0kl=HiuZTao*=B4*r=g(R+JF{_frueHB
z|Bq|dn0xR3r^YKiAxvXKo=x1t1J~{!NtU_tZD;?a>9ggOeW&CUUcb9s`pzo3qfrmT
zdhJW^++Xu2)Id1z)`M%ek9I8G|MO5<ho)bn`B4qOgsvw|HajD7R<&OiJ^5GZ=C6j2
z^KX4wZl-%H#k;It!^^B`&6Zmd|AJSjForL-%!v&;f42Cw$@2Q?_x|qm+uR?#K6mc3
z)LH6t*3S&LeIT5x$gRmXJ8<V54{>Apndkpk?fG74@p8j`3y;~t7q`TIUy?Ync>9u@
zeO!LC4Ud0*`?~e$-(Al$FIOHY<bE=T&m?ipwf*Ax4}LA&7F=?9{{^4=+a6Qp{@*<7
z({)zy^Rvp__my}1GIyum>Z{=Y<GY`8<K%-44{G<<7YZDIeCW%jHN2a1%sx2gg;Z^C
zE!;5a+J(q(GG!amFWkOmo*MYORfeaSEqVu!+m)RzU;0E|G51DwhWQ@<diB+ewpr6o
zPA{~0Z~5bNiT*UvUpK=qPtw>_8edlb%b-L4n!(wk8FjZ5H(J}W<!T?@leJ!2?{8h*
zHbbkrO)bay*&VJ&Zj0tS(EojM`P|aeyf4h7gSW3@{k(FEsO4NeUWWDh<+nSxt8e@!
z-M3wN-TfykeEx0}i0|onq4M12Qq%Py0k4^dYF_M|EC1W#4?{q5^)JJ2vxW9|YtMcU
zyjHIn`(N(3iO_cC+qHj{$~Ig5bG!6;F?*uS|F+}*I+ndS-@otAaoc-a<v-mhTA{u5
z^uk?wlD~i6|M%lUaOnZpdYke;XBR(+S?Mm5_4|UV%39|$o-@`YiCv6ev*K-^&pQ^2
zceifJE3Z-C!nruaPkrWAft){!Buo}eJvhhs*}oNO%bBz4YrQyUX&Q)L?u?H3^7x1N
z>Upz1Y)_x#uYca)!{Mexp~t_{V_uzfe|0pz{#Djn{jZnQ+mj1)W!66{v?vJM@rg$*
vqL-^lVfx+;k&8-8oz2d)FMcl1ar@)7b2<I1dE?zS{O6wbc2?ay9|i^h41>mM

delta 4489
zcmZov?o}3*@8;lW-@81Tfw?@R(zrMyu^_dWVIr4)edN|JQ<kk}kUrHaDV?nT(<88N
z(wwV&OTtdFahaucd8#v7#m-r;ck1rnqleG_f6~9beEat8KiTVxqx1fie!O13&(5}6
z!|%8I^w;io|0+If-hF=C_``?QXDcLI|Nr^kef;;F{qy$Ed-!QpZ$<es<8}Ae=B+c&
zIJe5F{>%OQHMjN{)SsWQMDp*|yKfKwtO=X`_<H!#=8x}q9=&N(jITWLQqy8uVUB&v
zX4%Ag+trdMzkZ#~aPw%x#j4b~eQJq;$2^{QeV>%F@5B60$A9nMeY}0M#p%mM?2l#b
zTVI<mN#(F|4WDFiuYu*Q>z5Fgh)xdiaD4`2fj@5(m)G&EJ$8X7>rp^l{r-z5xt?D5
z!Q)pwds3iTYs7?_O~($m{x|$RUrx<)Z>{wriFvx>O%Ek>4YVh(HJe!J@_b6Gi>AuM
zoT4+2x*2$5-nj)yJDfgoxlH1krTqPK;uUu*)|zZuvDodQVd4}uEvBWhP751)J=(-S
zRn5BU7Lv98zDM?6Q>NULN^Ys$#h2>SdX{Kxc=(HXhlTJD9_LRD`8%ELKOCEUe%7ki
z)N6Adak{2EN@+SVZc1qSyueHOkzM`C@BC}n?mm%JoTT`$mNQ|FfL7XsB^N`=cxG09
z`X*ogd24;;tvwTs#qX{;GNXxuagFAL$&<C1j=We?sMYr9@a2~GYEC<|Vywi|r*4%J
zSX<B6wsuWM8q25R1@jht;Vfk5X>46>V$EWfs(91#RE&X(var=fn@_Pl&Cc`wek^}~
zqxa)w$DLtz8>*Y9|4v_grfPqb?FX&{PhyVSZ)h^KvwC~*($inrRli;{Gp)P7Vbx-$
z_dZOom#QDGGmH*%VmvhIy0~v0v)xXkb!Eo;th!(7*E^r}^h}M}wC{teO6Vk2=}nVW
z7F~Mv=+*Rwx3&L11bn~0@@je2FTY|Li?w!}PP><wt?t+9&i|8LbzJ$z(TpwyZ_Q-_
zw;ouo6UjD|Xq{O%v8U|T`n~53y`q;Ko+B$gQE9bJ<V;sLKcTRQjHi8J5gCUL8P*=&
z^=|Ivu(%@q^;^%@r!bxUcG6MgfTeB^Q}WF_foZE%x@I0&t+8um)$M=xTm%!@e0>gh
zES>jn*3_nXk&f$UZ05>PSTx)G`1#vkwk+3o;qo<Oc<c1;!@Q&33lo{0-a5TqSbF(`
z(vF04IX$9rdyC$Bbulv*Y8iQZIGOL?v@fgk(0QRC*H+`8S?l>MChOO;tw=XW+qbE@
zVZr<>cHi8Tid(oZTFQ6n&H27##$JxjHO1MVS4=biGuN4^T9q$E=7pj4L`&8y(?n+l
zRP*+kTBYv%=*4bOCif!YOr|k|Idj_8)UGwxZ~a)LB$>9{Vj_dV=?7Cxmb&C5W^km*
z+dn^V$}F?Vb>F&oPpYOWetIhsSYI*2>UH4^yI^~tk8e|D6V8>%B(U?&WuGyvY;96&
z#=$JF6-U%Q91ux6V)v;-vGA#itlA;Rd3U>t9{fJdx#>1Tng3zi1)IFP4Q?LtoU_?7
z@WK;L?=Lzbo^D5z9xpPS|LHA%zrEkjMfE=_%IAOjt8m`D#qfAS#M2@*rL!+Zf+ktj
zXPoZScUo@j?;N@EtWD3a#4G8`a?i{VI-h*SN}jFx*i42e7B8K(4t7ZGnylf~_U5DN
zpSOzy8ZRCdH<>78ywcTWo6z}J8hZ=_<r$93X~=z4+`h+dE}J)>R-nL*H_hiXSf1~j
z6DoBwlym2gke<YR<A;mF9K#MxV-jEf(OC5I?EUp0q%CHjR*ze8TC(X~e2z)}j0wx<
z{BgP+bJxpkZ>!mFm0Yv1#g<BW70P0-7=DFUf0{RCN5g`}PkZ<cHgsy7oPMx6bx)Ad
za>qyU$Evo*9hekU|2<Eq-@8ze$zN!Z&$O9=R!XnE&diBoH&m-W-#DY?>zxUgzs$Q;
zeXAkD>(LprclE5Z9j|o0R(hUu;i$^9qXBEZX8EUD$g9tfNj!GbS$}QY#`d82tvhyc
zvd(R}Y0tMLu(ojLrLvg*YOW=AvzIQika@VwXT_`R9Xt2_u6b-<E0eT5m+6AH@5iM}
z&9-j5lwI+4|Ar8buVG*BeO+UB=G2j&cQcz;ue$r~WKZ23`K`x}FRXu2#oa19<BQ`<
zC6DDwdwq|k&2Bb3DJtm7c0En2{@=@w`}fN$v)7w*ZtyDl^i^K#cz)Jqr-joxyZk((
z+og6+IOC?NSnzVwU7H#ig>|v_?ZtvW{V)B0{?5(kKN9X1e!BkeGPD1R1mQzxwq{NA
za(%mpJ1qLqs<|2ohbFL^9<hINyuN>aeqOoZpG_OfX8npf+@Mz#-{&79?NJ}iv2yZM
z`;U)RRrlrn-56-|tw_GkF=qSnyr!tXp6t`(zbHMpJ<~+aQjmR?@qJ056|5p_9X`&U
z{WQ*S&AYbAFMiq1yZgJ;>Bm;JmZ`HtA0=+TYp<EL%ce3+U^(C9*M^pUR_s1)n|qb(
zeTp}G=p=so@;Ay?Z~7l6Z6-gx9dmfijxKz@(Dt{D{#3WnFGub3->)|Q_%L|ikC*SB
zecPCG=&kXAV52wI#Yr<7gYQg=Rari_hsSotBmI3peoNQ?u9#SqqQhT#U+Ai@+Li8<
zm16DE#%WElorg*zg}Ku^oEMpi+boW7E1qW+eZ0Q#spL7E=oW!K-+f1JtvlmYSjwxV
zIhRMG_~Yf;zVhuapM8AxuI!i3el5NtN8U(lZ$FnVrZu8-x^9ZBaETT2|91HCAtzJL
ztGCxgrK)A=6s<otXYb}fW2tFUHD5W7d~x{k(bxX|jr%u#X{vvFKmF6Int9w#zeMjy
zmz_=Nys)s>wEmLY`U%<w3T3w=5)S`8z&P*U<s}M%(Q8$&d<%<BO5ksqvvHCBwVz3k
zCW@GSy`ewx^cO~JZ|l>pW;<_8jY-iLzj?ZK_4;2cZ=X2&N34i*n(D(nr!;P+PF*6{
zv0CuL$;=`}naJ;jlfPLqv%J6HEgkA5C_Mecq)n%eHik7hSsEP3tuG1n{d8lI_SP3&
zwIxe6ca`bBPv_XIwR44UpXur{H=*gl%Tm^>Og9XCzBeqV>*sw7!HTw!a~mc(3pVz6
zHhMpi*~IF1omb3dRy4oeQpLpRQqzJ=&ED_Ir#ALTviGcRlUe%b?fvYedQ1Ori|%at
z-}C?enh7&_Cwba`?Kv_hwBMz^+{5mNzd7^0o%a9o7Nz`gww8Jp_O^U>WAXN7r`H@W
zFWtN8b<~^9PYMH*ybiMee82chjPN0!&9<_aa{41TepXqpIp4c!V?~xQV{g)ppgn38
zuh<Ltba%cHx0@Z&5PbVdsmYor_ll+k&*tIh|5<n8newA2!beKg?62k(bv@WWC7?dh
zn{!Tc`a#u}(-~a5S<VOEnkuq%(|xZQSC$-EJ#)fw<B#>nLq9Icm~dz(kCIrCMr^>5
z)X9?%dXzu#JN~}i=*!m+f;)INTSe&`cwN)z<7)jJm28=L;LX!n{iX-DRs7PDoUB>U
zp!{K4fD=!GQrhYyE!DO+4>ayQ+$L6cRp#2HS@kBW)0aMPcy0N`N>=CC63fi*WoIAu
zw1;&+`QQJ;RW^npe$KW-)$8`{(0VxQsEX6vlsjqP?af!c^bMK4DbUn?tKqrxUsf+(
z(RO?xL%E5K;MHBG9q~*5w3(<)jeLKy$mw9>p`wqcp9*>=G~ei0<<IU{pK&nrgOKsc
zBdyJ4TwP~^>bvI1N`5)^Ywm-(v{$9Srf#asU3q=|#8Q#2r#d?$bR|qX6=aq@2sv=T
zEjM)fi*+du&npYJdoRw+a?pFc?eu$}gqCZIkDNZr{!M=6S@+B9Of9)1wz5>Qrqq4e
z!t=z7t?0|zwWp+AjNYllIPa``+|0nd(?z~UuSQdFlMAEB6uv|C=7zQBzS}>UyPzuW
z#hq!_o_f5mRBg|@uIR_3|NTShn>Fu`-B}~LMf=NrKmK1fyL$`wPIB@;wq)tD=!cT_
zlZsD&$gNJe-8%2U*6+*_!V9&T@9DQ}4-<aCc6392LhItr9(}&T6}xU33-kY|%QeVa
zl+t~hNB5>^UTnF>nu6EI=I7Oa-uirf)69a^ym^;BGLG%iIT{n!D|$J3_Lbw6YRfez
z+U)LrKEXQn*jA(D>6$!m?`#e9ytZTO{Z;-hyP2$4E^ZOM_Ehu6OyAu+bFWK2$$Pvq
zB=&V=+3G@@Z~3=3?t1$`!n<ecgoC`lRV5Z$E;{suZGUTaxQWfX54$q``Yz1c@o{f`
zf|Mh3T8!3r^PM6qJ*1xsYyDI2{=UzQ*P<r!#Fw>Pr~UZqwYByxy`j7IweG>gMOP-i
zd#uMVQ@v+)M02qB>(i@LFYXC>&+lC($Fkvh@v(^4C(<Wy1%)YQX`W7;{i}Sjm=oud
z1tL#Ge4;s7lg_26vZ*Vbh@Et9pX2<x@=c~sAJxYeHcZ%}-Ec5#QPKgGx2{$qpSHOC
z(RyKSRq59-lTkI~S<u~}1utAK&B<x#aZieW?^~<d6LHvdjjtY8;-1v(b)f-XUK_tX
zPx!PwclNwO$MY2mcQ$qiFTdUN{=QkehQQ7;{*BM>E$H=raneQa`;EH?A68v?{a8t<
z&1oA)y2HZo`ZqU{y^JECFE&?`&3v@U`rp-!!Aw>D4XbYKdb3hlVc~YaM79%3vc6n%
z<Lu)FmiA9r)O{)C`J{joTQ@(_{B+7wzi-(}d)E)IB%jQ2a24(fG7Oq9%{1uQqNQJR
z;uDUXFH+gB<oV;@cTwjsDN7E8=e%yB6EzEal)o)=OfmEQdg)F5!|!Q_pEd-kgayo=
zdmu<d<is2%A@&^$>dK-%T7Q1L#nbiK0|%Fxo;wcwY+tl%cC72R<LP%#WvA)fTF}em
zu*y&PnNG8Y43ERqB;Kjhe@?xAW}#tMY}@o(SJxRw36?zkFlUqcx!v35ZC))E8*Z{H
zSDx)i(Ygh;7v3gisbBL|=@qE2{`*U%*^J|G*~~dYVIJ)YTmb?P3?x<O#YPt{x1X}2
z$(8HWwb;fmxB1SYat|(e&osF5_2=Hdx8J@xD({n~HJj-{jbiZha7+I%P8%i8*Nc6A
zPf1;JIP~CO&4Y^Sla6W08@a@;d72~k`dOLIK`D=wHx7#~y}v4OSFZo|y}R;WPOk6T
z{Py>fy!&cbYmMt)t<77;dTv?lip6G1%Rk)Jd3$S#$(!V;g$H)kSGF=o&lc$~47jal
z?-iF9HPs|=)6rP-jd=yDs}^OqMw|Y-QaF3dr|^S5J2IQ2^RJssGkeJ$t-8#D^`6LL
zi$+Z$#e$u2Ijhp|h@Si#b^F(xPxEhmS#DPPw|?Fv*{(^w3fgPU+Wu>YOlnwtQD&Ro
z%ID8^KAm@YzxVrpG4F03UwM7oozF&Rh0k3-vwEIz*R~0*BF$%4#P}`gp6P$@dA;qu
z-xe}6ZoIc&a`s@>Exq}dHiYepmdsV>TW&k|vEk3Jzn;|n{Icbx&4V42i~QJU8HAmF
z(QRJvH{iDBu9x-k8Ow5)c=gx6NmD!eY)#eYJ=?zT$veK~u2HW09`=9B?w`JKGQr`)
zzWZ#J9ghnWt0HCFBh93LD41*Qz0GME;hFtHCtBS4hVhHsx3f2``0K>iX4$M8!>0Ty
zMybl3>uaOiT9?(!g8yfg-g5R`{r0rQob7slQg?};cKZKjb*87t&H7#X*0mBx__JrE
zSx&ak-Eu?Lsd<}na@?QmywmIK?QcuS+D9IG+|In<wa#tb=P!=`KDqncuBU8YX3MUN
zzS{J&;C9y>zv*lZ*Qf7}J$ais_IK^++k)5gi$a$Dd)A@v=2kMPSSj;hwkF3?pF}(B
zyL}65W$N5lY_$EW<~IAn{CE4F)&JIbJ!M_}wPdNz+Y{gJs}tNEDO;cQ^5?~7gT8vM
zl=@4-UycXF|C3gHf9ri?j^&l9x1Q$2P4B7wt?pv?B}BI1;`~pt^;Vh|;jcV9Z`qY_
zdcGDY7E)V1!}W`}cGm96)2$i%X4ijPF8JCp|B%Mi%bsbvEYkZm*myHi4W9SxwEviW
z^W}l~`9V!-Ts}uj3dF_!TKs#sdb!%4x027DFBtRu*^tn2`cy=HQE=&Iqd6z;{PN!W
z<>W(&81Cb%D`n2D6<uf3%o(=0N#R7Qe$KRv*t^$xKTE#;S$?c+&(_8FA7>q&F8Jm@
Nle)*ZhNnIZ3;<Ur*^>YO

diff --git a/examples/coincidence_count_list/why3session.xml b/examples/coincidence_count_list/why3session.xml
index 76154de7b..1c973191f 100644
--- a/examples/coincidence_count_list/why3session.xml
+++ b/examples/coincidence_count_list/why3session.xml
@@ -9,7 +9,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="2.20" steps="9039"/></proof>
+ <proof prover="0"><result status="valid" time="2.20" steps="9025"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountAnyType" proved="true">
@@ -17,7 +17,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.65" steps="4378"/></proof>
+ <proof prover="0"><result status="valid" time="0.65" steps="4363"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountList" proved="true">
@@ -25,7 +25,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.15" steps="1018"/></proof>
+ <proof prover="0"><result status="valid" time="0.15" steps="991"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/coincidence_count_list/why3shapes.gz b/examples/coincidence_count_list/why3shapes.gz
index 39299431cf0dfd6d4a293dc1e429e71f6063038e..5e086b0d518ad9e990f0e907d6a67ec8c5105eb6 100644
GIT binary patch
literal 539
zcmb2|=3oGW|7WM1&bw_O;QIY1SM8w>zD!@8473i+PCK6KIMLa`K_`4$*OvPDS8H9m
z9_mG<lv_TTd;0i92Vo6wSMS9$E~%bS;AKfW(0!@8Yv$@#5r0qZi`ekRg#Sbp!!!|p
zyI%}koCzLjS}qLhHC&P^OjMuGv`zb1boS5ERkflUzWulxUw7^8jb{ZLOiqfe=ZpW)
zQ(C=wgGZ5--0D{wxBfY2v@^?6-XY@Ixr%MKRy{vCn{AQg>MbXp8<py{JPG(YY0<kS
zAJ%W)+HD#4YWCLEc@_UI{;Tu7{Xe5kq_Y0Y?WebrHn4p1bgJul7yZ?!n#22Y?c(s+
zedd;F%nPO2{g0kxJpEZHyNs#)Ptx2ScY>Un?DofNmv7>8zE<#~Y-hX5$;@gdjd=%L
zbtH@QOs`rky0D-og)=dg!F%FP?R`93%9?x@Ef29&Ogg#pgPVdI>%GjEi{0LZo@A<X
z^V)s(f3nlYmqMRRSDuad^W?}k|3C5>zSA!ropUeYw$Ic355rmV4iu`+6%VO;HAAUS
zXyKgBd)B``$WOO?Wuv-LWS-l}tyk=7#f&oEdMyj6KT~v^=XIGWM~0hYcjNs=&58X?
zVyCJS)mCp@CFweAmYKTvmbV4XE3fSJ-fnbv+Kj6&{JI=A{!!n}CcW*_?Kei(uiqCw
z{!U=}w?pp))y?>(c3J;FA$KJAkstHkzMAH_Hxkmz4qdxq?{QQ9Wx9OI4R!_w0BDE}
A;s5{u

literal 564
zcmb2|=3oGW|4&1G`)?}<?0vufgTDluK|~f`Scvz|lKdF$1I;O!kFRvD&i!Bev3!%?
zn!C=cr&d+-oT)zi;TYT51D36N!7-WanKRP@KJn}+xu>kUZI$y^?Vm{p9wf$Xc+Dyi
zX5;xZf-_}egE!|=S58NcUa>V>X8N76<6K_+$UpS$>PcDt_y4|3zuRZBd+tGwXshU|
zh00go9zDQxGjad=Ro~}|N*}+Zed;IErGn}ui!Zv_`tK}MoNd_UYS(`8)}|gwt@w~D
zZCyXCmX{g*4z4wP*45i*f9wAGjep#&*PQshI^OU3G_S)7^A(=_PS_u+U(ENoaJPDu
zY1`AcpKsSDKFgiKnQqsn?IgL|<n!5wKOXFO<d<BaIKTIhPucP>)<Lh9eaqFYb<Z}>
z;LXjM-sg6L@AYY?k1S>r9;>*l3ViJl)cmROcw&I$gvp(@mrp<V&9{N`OCA55;<HQ&
zr;IF4Hx-F+&V9^r@bU65)!~2Qzgd~ib*g*&GmYn;`MvjNKk?Vd-@bKHCXa2w%tP`s
zSt7f5)&#8lDiqv5O*?I(XX@q$dykg?XZ4Z}Ryo3NXSmK|iJ#|t9YL;;C6|r|U)<SW
z9?HuwOEAIE=g<Scnf(l6`@bp74l-UmOYq3rl{-o#g^WuK+IE${^gEV!QnL4^prOXJ
z{BrjVMVU3TcfWi4IDhYH^F7kp52Npe-o7_g+v)F#-9<-bt<~SxY<ErHTKYCyw`KMt
Z^P>~)3f}HblK=2p-d{wzbQ=c)0|4Gf7DoU8

diff --git a/examples/gcd/why3session.xml b/examples/gcd/why3session.xml
index 2584abb9f..3dedb4ed5 100644
--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -89,7 +89,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
@@ -110,7 +110,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.01" steps="17"/></proof>
+  <proof prover="6"><result status="valid" time="0.02" steps="17"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
diff --git a/examples/gcd/why3shapes.gz b/examples/gcd/why3shapes.gz
index f8faa78effc6d32c641cfe33163dc0286a6d8d5d..0d6f5d306f62a6c77656f72600109232bed4cef5 100644
GIT binary patch
literal 1789
zcmb2|=3oGW|4$>m`<2c4_B{{(vCW~0LBw-!gAYUUL`Er&G=1)Pb|FpGV`;ZN{m&<C
z-d~qletX@f)9d}d$CNe5O%D<J`BBl%>um6a6E`iDJR0t8o_uAGFU!iE=fvvgf4zEm
zP3^S%)1sz*ul+gy=5E$$@h;*U3d&D6TZaGJduz|l^ZE(j->}>}Ki}PcU-X0n2~WN)
zmKWPnu=}93VU>M8=XraclXrXFCtt~7Ird}ri&m#x4c{H=A}?cBu$8RY`So4;r|ik~
zXM4^+zaO^w*Yh{~-zI)d%Il0_k7rg+Un;jH>8X@4$MYnOwD?npH{G#6x8<a>_WWCZ
zWj30>b^mAwES_ia+hJmCmZ8_8N1CNvji29qZ&zDg9c!l-{{8pfij2wPhW=dHGmAq#
zdu9q>56fNmEyz@5*57@<zEqs}yZ-0ZN(UB}eSsZ{8;`vZ?#@U%7QuDp+OfWU&;6oZ
zZqGb>L%+h>KH-S+wz?PR_8ge#`7!VKLH!SZ>yAiUo_xkumuDu)`_3&PWBs<Dn%0+o
zJ+SqY-=;1aTd+({Fl(7ychTvCp5Go-d7YfC{nX<2!P`<#qYo}Rt-nq7zs6hd-SKZC
za!fXq3Hf+xB)`>rE)>HXxBExOl;AJ>WQG5}o3Ueuz1^Gz`ZqQ_(L2Yt;Aj1dKBwZl
z=EiltE6=mN-u{Fy(`4n8#j@d_a^$X@ZDsP*JovmtCdJI;sNCHEUhDgji|_sV-f=eL
z$-Vl+akWcb7;UY1^r9DVIbIacdp)7F^JTg7vq$r0`0cmmZwV@S68yqTF?)i8OJg(Z
z#R*v-6IoJ<y{<LP3*9-bXz8whGdG=AT)*b*QjTMXHwB#6bIN&E-0RGyd-QFk<lpDd
z->bJU6<%I6>)ZVD*li9iSG0D#x#D_eW{%6<>qoA{EZD;>uJ+D-a^YX|#L24@c(2vl
zbC|HNezxB6-<y5;{y{q)Sa5G|_}TbxPbk0QmOIT68@^7=a({Q}OzDCMCYzTQ&b~b{
z8Go6d&wTc7%SsM5U9o$*_Z^$NG`)>JPuXD_6?<=byS@E8QDZNgZ}~R1tgj0mAA9~?
z?pvPl(Oew^$2Ttvc%HdGOx*p*<m5#jo^-y+j}nFM?)_W%_fOrv>0dS8T;3rit$n+z
zNqOm;&sP~P28Oj1hS_M9%xj&eVis`l$6rrHH_IFTTpPn4Xue2v(c$Yn>YVg>?>+H{
z^1DkDqmC#q)1UI^hUl^P$4zf9k>t~Uf4JFn63@3u2N$L|U$=_)O*yKxvTMsFtAI?t
z#jUKz_lEPU&e7|Q=Xv+8s>J7tVzF9wgG_0k#Lk2(E+JKC{<%D?S#n7_V$u7ftGKp3
zV4aq4A*7zZQf|Y}7oF}p=Orr4cQvJJ-}@Bh_p0mJqy?6#o{Frw9bvk2A6C98)o;JJ
z)7)8*QOhH5rxk;EvqsTICtW-9)H17S^Lb7LMwjuN*lXpcedtVT<XVHbTbKJ-rf*!y
z7kVb8i1*lC#`^3HPYg|1x4aWJ5Py|r%V*T|ZENBAFLT`k>ne5>)bCLHb@};>Z&zDV
z;(Zr&Xz{5oNwIBNkXjx1ZSUfkt9K?HxbDu^yVRk4Q9zfhX{X4_)`(z@mA{Lo?ys-N
z{%Yh|elBun_TRZK4%si5f4o{djf?B~zSucloAUW~MayL}=<o)tebLRjAoT-7q+^oB
zL*ZmEjd;Pr6H~jgqS+G{y$ZE-{(3K3KSl2Ddd}bL8xI>U-Yg>E+`+Zhy+3S&`@6no
z#mCc+JqTx=xmk7jz1`OiUC|b7&#*KO>ObgHe@)$g>dbt;sFg>fVso~-a(nBUrdkJF
z+G9Mse2<pj!PYk)S9NR*^*%8xHcdyb{Phwm^VRJl)k*F8eg5maj7%MwUd*vo-^4L>
z?baCiYR%p~`z;-8&)aM_%I}X?wf1I`T5NUxfwf36hvv~xuduv3BCGeARrKGn@f109
zZfl04XW?JVt!aAKKF0ss@w@&?a=gcu2{l`*)^@%>`Dp(-dn2RkS1uf%_1HC3u6X|a
z1N*Yqbgeqt6#OCM=RB{}=S{-d90qp|)P?Bs-MWyS5RzR{6(P?oulqg1I%w-uFWcQ&
zeWgFQJ&3YC-_L7nzwOJ9wwG$2S8~#QnZ$fdJ-Q<%TeM$sU7OkQ)~))TZKYk|s(5j$
z?GLgi3M6mfQ#aXU)pdqXCsZ_e-&N6vb1tbrx)|TkcjDxSRZQXc*VgmRT3YTUx+dhp
z>_5+43}#*V|Jo~Xt$IhR^79$h46n1+i0E9&xt6uz#`5<`Z@(K}xc}z=^4+TrO0b=8
zmfmV?edoc<=fcuv*MpZw{MjNrSM2bHALrZ8=N7!RzVWC%N@9{!%>=Ff)%~-#-fj;x
z+&+8HY=_t97v5F)6%juF{nyJoOPRI%8TdXupWIQcFIDsB=Ds=eqiojxy;%EfOOo4X
RY4%_8E6RPQo|R`{002Zjd|?0p

literal 1804
zcmb2|=3oGW|4$>m`=w9v?t8!fg6;u5v4n|h#5cq_a3m!(9N5XSODZ%aR4K*ymTZ4-
zPF<}=rAn#y+UskMO_z{Zy?WQ`9~1v{^}l<jnepU}jG&6c`<tFw_tcuM#H4rIpa1nL
z^P1gheQ({<$M^j?|K={!X?qv(4F&wCn=Qlt?Y(v9=6U^u^0zGa&d0mi?~k5vAmPck
z#q-6s6zo1|z47nAU3V+~CGNO;xWZ)T?A`+`_2PR2R`4$6{NAE8m-}i%pXv5{e|`Sl
zd=hUw`SZ`|SJ(Wr`<-7MwKpnC>H5Lz2Tnw;WM3Px^BB*eof2I)r+?a_(|_JL_tTYA
z%eP&Y^?y~@{fFzy3iWe#0V&g?dM2%?@S5xNz~=YYl_y^XPCtM8>f<_HxnEC04^2K4
z^*kn2DEZlut)a75?+xMYOxwTC&Q{**fAStH{*HzN=3Is<*Cc9_1kaw4@NT?yYsQP}
zms?!7%)Qz3w`u!lW=9*L*X<?GSo>nS_^mnX8sC3czW2h@%>2R5pD8945{(P@-h8(F
zkH_og?>4nJ_RV_1G_%TO#mp+5Q@ZTxH@jbJs^*8BD%{q*z4X-gCfDilIhOyzZcYET
z<3{I=hy-6DA5V?sw|dWoVtC_r|LB+!{AHhP{;$IypFOJkU653NuuZkRu#BPi|3Yi7
zv!(aX{4`x^CvCI;?z@71wW&p09(&E}b-b$~;^D<<r~X7?^Fr-!FWS;>6sGr9oqj)Y
z#>EqR|M%_v<<-elRU#3y%|Wzjk^Y@)imxYKkZ(J5v{uxr_PvdO*Tsqc3$<I<I5G*c
z@`<@PuR7W;IN_{jBy*MF)2P!^U;RoyW#7JOli75o89b+*Y<F{PlzcAL&J)#j`}C&2
z@$2g61aKYkU7dBUKC<*CvtZEb2b+S$4bwLXmc|PQ7dL*=i<z-Y-uL*|`z`+KnoKMH
z9d}${S&>!O|MvX4-~XQQiFa%+;GQ9W<9zg20jJZp9jwvvE6bkfon66vROo@{BOYDD
zMHhat>v60tJJTJ;zc8soGI{&1V|@PW_ANOUz5MFa<jP-vAKx=rd?fk*vCF|5_{8%p
z_NU+2?JKf<<AEb-@%+aV>O|zW`OmpmWWs!S=HVq3GhE8c>*M10&wpQP%k|r2-LYfG
z+J1h%UuJ%{aA#4<##$rk1GZi>4W@9q8-1UpTcJNs{pfrVs|}BT{PXng5!$)`u28o4
z+)MU7Dn}PCsqp*1L0oE`$S<$WGLv&_>SILxetp`o&E960^4Wy-k}_FlD(`<*scMUP
zhAx?Ut<kGkLidBkySs;+IhS|84{xsCAtx(bdScGWC>{5?%5HiRrh-%DHrofzlArm7
zZQ_gSjk{VyS#%Z`s`#Dj;ymzdk-A)`&Ep4mUvSM_TXA}h<x1^Y-c8S@sJ4o1QH-)J
zb9-j^I*xyFaekW;Q^<rnMWqaSY=KXbmL}9>{(e)UV=p;j@v-+36Lwp>X@Bn7v?lD=
zw_Cx>=4`$Z(ysN)XeZm_cMbbZBR)yYVv4Hgp21zZRgX*3@%OEr=~lNN+Zb8I?68j!
zmi^%E^E=IJ)B0tBE~4#1L7Vhk1*AGQy_bEu>f6k1aX+V>Sh!K-g`bGm#>HwAm9`3G
zbE%fbuY2^n-JI>_X4dBdT@mLli>x`Nr#SVibhBK|lg;_=aZ?-b$0>Uo@ir`F%sM5+
z?Qr@5<EEw~1x*Hz=N353Fn7;6wrtU@Yl5>@RE3@k*!%rjm*m~wrj`%oEM$zWPV*bK
zthiA1CF8HtlXn&pMs>Lj`?OCqh3qhjTvwvX;JQN7S$kv1x(P2#63>fmn%;b`v!gKl
z>6EB7SC588Z@KX-D3~wj>g4icy?x=V);lINz3Y;Q-nwSp&D3L$iu85n&K3>rvfX$%
zoPFo-Np9BL!URmsu6o_;bWP=vT)M*W#k#<Esn3=^uBv_-vT3u)V#8IRdG<LQZu8Jw
z7qqGA*|LW3YY$dGd3JIWf8z6~Een?Hs8fwGj+UBqT7Sj={(HhPE2b#?%o0r$zCT%2
zFm}I2>bjK+`%RB`FSD6ux8JemdW2|bx9hqG7bA;P6>si*a3qS4$Gk(n^_k=1YTlkK
z-BAA5$qyE*8e~_j+7`4jJ-jz!`u>WT*Ux`$T>Sj_Jh^(+-JZgx_amj7Sc7>lDP2=J
zr&t=8?VYsy;{0m0^Xh(IYZn%C?-S!RWP82PNm={Yi9ZK|LJglrujF{%V<*`EkD<iH
zuPt13$FDrustY=MgI686mU#EbeBpx`m;Qafx+v<pAh-KD!|x2&%p+|hSKM49TC~x>
z-hbQu=MMFo{_n5Lm+na{u>GM`k=805^SLJJ;4|Udnu7H=SNe4)M*R7G`MKGT65EJJ
z?O_smrWH>^=Y`9gpU=~G`&n)N)1dL%eCOScUpB6@vwyX`_&o0(8zzer^W#JBY|i*l
im04X}_v&Hh>;8Qw{iM@O_A6fa&v0~lZ{|b=1_l7_PKa;-

diff --git a/examples/gcd_vc_sp/why3session.xml b/examples/gcd_vc_sp/why3session.xml
index 069c0e3ab..63f373311 100644
--- a/examples/gcd_vc_sp/why3session.xml
+++ b/examples/gcd_vc_sp/why3session.xml
@@ -75,7 +75,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -96,7 +96,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.03"/></proof>
diff --git a/examples/gcd_vc_sp/why3shapes.gz b/examples/gcd_vc_sp/why3shapes.gz
index 433c08d2322b96ab9568009f2ed43bbe7ca81f19..df6840b412c863c2b163054087787fcc7a8013a9 100644
GIT binary patch
delta 1654
zcmbQr+rc|Qwf^1H2iF~xmRdhvxBG3H@Rq+{+^u(iJ0Vy7w!~atJmK*~H|Kvp=FiDI
zxY_O0xk`Rc1D2vmQ5$%t&3c{m_3@(nclB?%|9l^H`q#Gg_3?Wm6Ms&B!4>u{t#-rn
zQ~Kq%t$+U&eY0-vf!j|XziKzv);EaU`S;a(?fpf&k4hU>+1m@o?W><XX}4tf<|{d@
z$9_nMUe`F*b75-i$9WcJOlj)9+7C6}EKCuex$X6aMa%zkDofpHTj{aoQ?tjvwBw3v
z{@niCwQbR&x4tQ+vAo^08GB^sF&e)TH$PQBBm76Y=-lx5w}K1P?k5Lk-P|&*dB?mU
zE+5O|NBQneKDb|0XV<@!{>S-CYwNSNua@mz%hr=|Xv&fFHFuxJ+z92nrRws<@~FTq
z!;A0xI=g?rz03KliP!txBaPMGy}Li(iQ(6scxB43q@sVFcNBZou0D^D{^cO&lt1sL
zx28;yQ&Oal??!j?(8K4-%~s4$N>4CebLV!xM#c)e%3}?DH=p{oMjDD_h1Ascy(|x|
zfA+}Ec<%mkxeot}KPT*1{d|qio4x5t>w1HA8`%|ZYuse03VG^w%KGZr^K)wXDpPay
zTn*%=byk%LCK=DqJ|ekAWc%~fFY@d6&llu6a<)6`R(;K@N^TdAwN0n}Vvo$(yS9ek
zbYgyAZJz(jLq}@!jq?7b<rE37Ir;OwdgrqTS3cFNo|s?z?)GGnd4+SPMj!m-P=8R1
zqxke()hG@3c<Z3;A*V&V0_<K|1pD&nZTZ>w*{8VtRtQTZcc-CPMu1_eXWBfW`8{FR
zw?F;Y|GoMskL%fgy|;@u@X6o#_2=H<dpVnTtYuB>sO9TB`EP>UJij?=mTwM}Jm2s@
zPVB|qyYgn&^XsQqNA_RZC$If!Mb3|(5t_fNOdU%?L=)F^xwrlcd=Z%>EZXzkpUd#d
z0|V_NZjH+qe0I?B>pbe5bb9Z-@IU=`E$4}U?06~eRriML@!yTEvrG>selL}XXinKM
zorh0#_O5F`^OUs3JVTdEy>@W=GlQt8f-BX$0Tmxt-dTV8?O~_c^>?;^TKKoLz<l~*
z<@eSpr|!*4cy8_56Jn6{Y2TL_haX-4tyaE$S6#&YyYm8His~4CNs48S{KT}{T*OxO
zbvSoIv0;T&#5}_fd8Lf!!<w#copVL>tg2(N*CdOLW-hO%o%>+(ZI^!g#g*pHf{a=o
zc{{Bb#3MykMl2Q+|MXt%e`G{`$r^i!39f&WKc?^AZ_RvSuZ3Iop);wTYYpFSUH+!{
zTvD{`su?Gr2=(k{sL$PCr(n)nBFj+xG1gE_h2^dE<3}$aSe^QG`N5&uf`=#Pe7oAR
zB*A!gYgd=^!znp!0$Z~5y%v^F5jN~<SAF+dx!o;jfpwt9Q77L;{rd{nbb7y97*qe`
z{rkA+y-$`}KVNfq>rX$WgrEct(+K^eT+3@Y{KamDv)^6YXTmUvZN;@ON0}}du{5kv
znCSoGhzI9WZKY>1wSl>_Ro>L{u9~v2O&~|isQ=ycC4Z+Mc-V0vlC$GX;KHvG7o@&<
z+!d5I`gKX>&mx85ZI7;0UynNReOGOBvZ?Vex%!(v_1Dz>x6WM87ggK6b=Qro?rGCv
zvb@9sE;Sj?F5jc!f6(~qV^_iC)nOA%cl$)dyfgDG&AP^~`OSrIzlHr?jZ;@xY#o-%
zXjGmKxaoG<_l9?-UCV0WE051T*7*GEN9d-_N(&5EakDIRHf)~|6!Z1ut=`o|SFf|l
zPl);;bToN+ebkl(OEebkOw%&^s9(4D_lJUxfB#F5)h)Z=#C7%8R<(udr~mJ&Jn0b<
zd{`j6@BFGyGk$;K`WBlU8lpRGj>Uqj)$v-E$Nh2?9QHN+y`bxN?1Fbfh;)Tj{vidI
z)wX7RA-PL`&5JcX{^@$g!!>iKA8(73i>~@}s$i;0*0#-xjNHrWPhC>FrgCoK`$c9Z
zN6MDkexJ8zPUoxXt$w}Ex`zxm`C8oB^EL3^8;77!!>8G?g6A}A)#U%OzUY|3vtBEJ
z_wKXwYdU*>ha8Mz-FvFuPi1lB-~DSu4&0R5aKP5>kWBK?6A`Nmwk0Y?HXHx8Jy$1x
z<Nw)z^(_124?n5;wDsK?;k=@J-_tYMx6NPfxA8}&nd`4l=YRL-dhnU6=hwyEKT|Nz
zLHI}JC)L8Dw2FB1+Okh|t8MP=y+5yZmqgX!yU%1;?9~5=UHo13{bQK@9BcE!S&R>s
l$g~G?E<Sds@z|kMso6j7?MZ6;yVm|6|L?P2+Z5y&7yxRXQC<K5

delta 1667
zcmeC+oyt2wwf<Mphirw;D_1ji=b6ubP&I$wmd)GJ-)y{ouj=z92I+nisZYoMKj~pR
zFQjSx+*aj)z=^F(4w~(_8k64rKE3v<!R7w9*OyLtS{wf_|65w))BV0;8w$!#H`|8S
zMd!YI^Id$y?lRtc=jMmq-y8XZt$FJ0_5b#M;NBj+C)4fyaovYMch@WK-2E|Y(yX-y
zB<fWkO-VY#5qm@Qedl5!gWbzwIFBEa^D>)|xtWjq);oTQiygTVT`t`ALMQLPwP<Or
z-yMI^Eo95y#x=`UUwo9ua*WTvLGrcu^;7k8!hWQS&JB-$E4VQ2ezM@DoT$?acg_pq
z^07RAlkeWO2l3`QoBpKqKbCj3uYdVB>3Gs&M&(%sOP?8Edsn3QMvMKWuFDt8qXJ)M
zyf8n0WcKgJcR7FYih9308z?q?%I?o=*0K9u$?~c-v)Hd%?%^E$)iTUg{)F?3S2Jt1
zTb=zp?xZ;fzq!bJb;IYmrmu3}^xWtPd-pb6L?vXtO|nD#o1*21bR@VmMdRlu|2jLN
zzOs1!Ouzfq{706*sPVXSv{)?f&EE8+b*ENNJD{vETO*RWD(Gp{si`M^rJu5E-?M3j
zw_s0u>Y{nEEi0ZCd(Cn5Dy)uk`~ULSZO(-Yc4h|p{`U8`&2QxJ)ZX#ti0he~w@-Z!
z5UwnJvpMf_Yv=EKDKY<jZ#+?oX#RYkPw4Eyl|OasPt31<_j<C(yuvxH(FguG)F0I1
z*!=9AZj^?5ymip_kkg`Gi)$_ww#|~*dEpoPyu>KoGu>AhVkYWdKc2VsY?J!+fJv9G
zWt3LN%l)g_AAV-ViktgCeiK=9nBClN|Mv~%vvu-bvk4!uV?UlyKSgevy5D4(w+9NI
zZ+IXl_Tui{_t&o1=RdEG?7y^6KK#kXO^N@0Tz<FATJO5M)NS$2jCU4K;&h%@aHLrO
zX4AJfnUnr{E@QUsdq4lmkrfl#Uz=_;yQulI@`xs%<<a6#pXX`DpZL<6Wm&fE<KIGI
zv&_?n|GhIPai4TB&d6d)&Wk<Ie^1qkh+4Ha^CI8A6^AoAj|aY=CdYNY-fn7p>dyK(
zo!i)T<-fdd-o0B!w(`DW@V9Ge*7r4&mNW%U`o8qIOxk|?jOe?kKNarWWxx26c0|&P
zqrb!^T|1y9<?4UZ>JiflJvM*kY3V$BqGJyPdv7>3bMg+Qohkw9SA^8XT({J{;W?kY
zzS^?KFP7JpWyOU}&t5UaJW=yF8g;PVBHKRucWT<jjeimx(!QR*`TuKTDcgkImTuXf
z&!l>;`TBP2@;Alj&Tg~1lBSkDJ>d@PkL>2JjFGGtN*T@^Ek77BL14-H-tOhiuXptE
zG;x1F*s5N9OI&zTlW(h-)+HG;zmv<Rv@N*M;`IK8-w_Qtv5WfsGE<@&-_3H+6wA{6
z^`d@ivTsZf|5K&<`tPR{s<%Bk6Eo|ojb~15*~1X4=eI0ftR6f6*u?ecmr&%yK!z+X
z4bANl3?|MDCzy0UakfhaA8I_j$0{j!o4(Sna~JMiS8$Td;yCDLSp2=t({~3epL@%>
zSI#MYOt+F9W{WG8y62pDv6S=IG6n8mPE+?>^$M4$uW6ZOl+n2~sP&1z^_!b+-+nGB
zS4zGUV)0QbyEJgM+v!}rl>(DX{SVH}FWIAU^PsWni)9^wt3yjq>IsWYuU>e~bL~o@
zH=Q#3EKc6NmbqkcmgAHaN>|yh>u4*d=eV9}&YSggUfDdgb=SrHqRPV3RNM+16-qRo
z>8=$Cuie!4Y*l^B_oWBfRe0~M>Obzc)#Ko_MUv{*eZtz->{)MTBe&@P@_p(R%YvIk
zR+YBga`F#zN%^~I$_llk0@;1%SAClC`w!Q**d$RA&1pL=7HocaDri&jn_0awC&D+#
zFMW1!K{aPjmU8IxQi+xf)-!DLw4zqMzZqJrQ{O9g?p9@8&WoQLm)0MT_gXi}<xH7b
zTf)JRotZ~w%_@FTEiCQ5C@%B-UiI_pi+*jp;Awf~l7-tg$*!x>#?Q|3U0KDktY)qD
zA<L!yPZsZIl$|)~p(x|3g|}PIO^SYR7pgFO!@5uNg->P#{og*7$s$@@e24q%hs8aj
z%E@bcH}@)gCjOee=&#+T|I`2eXQ`>%-*)ipgYL&O)$cr*^-P#Q$8O`?q>qPFy1qQM
z=a(;?BJ<Ag-k&}DW<RiLxb~p^;Pnd!XI_*(_;7QxdB)SiuXV*`)rMK@WwV0?e$4qG
z?ehNhtH*n5EXwm9m?$?i7s(v+lE~JP$<T>ewz2WOuXfs&{U49-XJFmgzVC?~0|Nk#
CXI&5g

diff --git a/examples/prover/ISet/why3session.xml b/examples/prover/ISet/why3session.xml
index 0e09d53d0..dfa1798af 100644
--- a/examples/prover/ISet/why3session.xml
+++ b/examples/prover/ISet/why3session.xml
@@ -74,7 +74,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="32"/></proof>
   </goal>
   <goal name="VC merge.3" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="VC merge.4" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
@@ -86,7 +86,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="33"/></proof>
   </goal>
   <goal name="VC merge.7" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC merge.8" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
diff --git a/examples/prover/ISet/why3shapes.gz b/examples/prover/ISet/why3shapes.gz
index 88f42772d6becb45e6a0511b21eda8a1737d1c8e..82bafdd5bd4e00c15d5c38d474d923bfd76632da 100644
GIT binary patch
literal 1791
zcmb2|=3oGW|8FC2=P6tA)t(Q3BJ46zNOeIugK`FQo#(w*r3+s7ZG4$x#hLc|^K{Yc
zuBp=>n=HFHo9&rmL(HxZAC%;RI(?q>6dOhh-%vZ26<ZpxcztN(zIS=+UO&G4_214t
zfByZLfB&-lL(Mnxum0Wsy4<g{N_^iG{kiWFc5@z{#ka5TaKYyvA9PM9lz$e=`~Ll`
z-yKu?GY=(-Ez*AU%(boACTqI<^2L`oE+$?m-C!wrc&$Xe#rf_TKaI;5@ZEPTT_^aY
zkEQUrnfX@B|M9X8&*RkpYadb<xvd?)aYskT$(E?34oSn}s|<WSy<dN=|FDIhU;p~f
zCCi28oxZqJt46wy_j|aT_~V+du8PsE+d>R7M4#m3Fh#FF{JFTY>ZZM2kJZU{`QiIm
zPJ6aLu*lkQbh5vL=AxBn+?Kz#m!BVh>9O-Y{q1GVrXf4#_X@t7eoTP#d$@?EGpCkB
zszTBxmla;C>;hJ7JG1fgg~!#lBGx-*Z#m*uE4%O2v3FJF#<~}sS@uS`|NHj4(o3gq
zOOMs=O4|w6#@!DCdCIp5CfoCC*G)dLK)Cbr%lUE3)$jW$n#nx&PjY&c)72TPeE4nN
zY~{NpPxAIz+}2*68|HE<fra5phO?S;XNXtGroAGTS01h^*ekHE-1rVN-`$60j4d1!
zwz@vwd{}6%poOIf7pF3-`oqs5vtCG=J-R>Xq}1l~S0&DF+`u0wo?BFMR8qJrX7=I<
ze{VB3&%N2BnZ_q!&DQhQN7!H)uSAV?LIK~5);3Mya3{m1X2*Vn7!|v`_x*H`&A?r1
zUu|mH{u5IpBNh~yav4|$Ov%0$=GoOH6BE+1;_wWUd8eiy-+wB1_0O~|$Dgh-e6?@c
zyWG{!mi*bZ?{k#-y3)r{+o#-*aWtJ6@jp9BcC)Rg^6#4_1(Q6E#2RcqEzMoHv%t?K
z%ba=Qd<W)>6LW6lO)F+*Z+`jw+GOGAo%5%7UEwMg5La6s9OhLyJNMkXDV@J&NVi;i
zxGmm;@#gJWIh(eson)9}aMI!G0`7vMuS&)1p6-`($>y}ZF8#h~icBT<tY6krr3t>F
zik13PX3f<UH+s18%X_1aD`{q;tB-I61bJDe%@q!xJ^5qTgWWtuzms(iElHk~U|_oI
zjhCvdjc4rR?sJM&R_PNzKiYp<MX1JAY5fz0t*hNO1%x;m-1OR;s<f|L?ObZdJfXBX
zWqZDETW@{cBGGjAg&Drrj9K)ISiDjVR77sgJ2@-B$HQ>5L4ns%Z_&t_6<3|6av4wC
z6Y?|YnvJ`Ryj`|lPS6SVi*_s*mZ=@TBYt$=h20!nljUYU@vi(;K6B+4gB>xIUOzf@
zZ}GpH;phH($JvId@7*rMw;x=z@JG#_t6tA+-%RyOx}md}aZZoJ*4nAR?#%G`#&>tR
zK<h2PGdkz2Tsd~kH2QznLdxOW{SBhc^Tp?7%uE#d{4&5|OF~;3Z_e@CPwV8;c6@zm
z5uhx}*J5G3sEzHi=ghTRb!HgdPWz?j^Xz@!^{&UuXT_}L3Q&I@TwOPN&5|jyI*WXl
zN5%eLd64JUHao`7Uy<)_R~2?|eVT8X>>+Zi)ce=8l@Ir2+_!oe`cBB2@2xCXm<3b6
z!5K&U?NfT4H!O_dsaKIHobmeYo=1=F&U)o_E9K0osVZla)ZCr4F3s~2oMT$8ZMrFT
zz5257M$vT>7UbEj3T29Px)2g_K}JhT*VFlwq{j;%KgHrNg}h8>1<sT?COa?r%-^V1
zGi&qus{#_5TSWv!4lG!0bV++fXhv`8E%UzcrrZzy7X2UmUA`!P=#G@_j^sY3lbaLb
zbYbbPh)6f5_~}~W*5P_tcTeT7v{+fR<k1mrdnebI!M&68X0|pK73LgCc6cPK{bUML
zoCdG`jKep?w>{uhXbh3Ee4e!6#(~!4Cnd`+<VLmdubwecfG2SGKS9;tH}Vpzf`ir{
z<GDABdwPuTrMl{)^}qjLUB)InC4G}mmqqaj)msx{I7GOAbjvoTtTm0xzOX<3;ryc0
zi#|A(y~$P-S#-k6?Qxcd8rxE*udfSNmhEpc=B*N4x+2`ORp*_t&h`m=%r2^A7Jb^4
zm-fATrDX9{MX&u~OJcr@wlL4}U&kP_eAA=%oj12#JN!7PKl;*+zaD{aYD=y~Oz>)+
zlydD9qpr)fQ^8(=@maI<H9rPt39SpUQE78JX4oYyxRZrnQAsmizwI^q<>QO**w0<G
z(Xt}n$3gez)fOGj<;y>Ow^7}*JMc)~@w6NFdS(CL5G}sk_|bE5hSh$_|L&%5-p>EN
zuTS~@n{T<lukC;KcG<q7cOC(HS2%4hG*4I=IPGG?hX2>TomvoWxT7L^j`W1<?BB%B
z-0{Bkw&?#I`%6*NE6z1fvRs;fBE~WJ%ZUcLBCR8*!j>w}sSdQSWV86J@#(zr0sksC
Si{}siGp^#cf3rxAfdK$%;c3(W

literal 1812
zcmb2|=3oGW|8FC1=P6tA)t(Q3BJ48p3hN8m101&+;wNpdl6|o&ImhazU(?Nhe^QT@
z2Ht#X(aTw7d_ajqVY<q_lg?UEO2^L~&9R7>tP}QlRkKv>+EX`Pzk9aJ&Mx--{L`o3
z_y7N8`&V$@p??eC)yLGo3|U_OF#6}Umwel18_aq6;P(z5^M3yGMLcEZ`VY(M@83BR
z`?;Av<%dJskDj@fHD<D=S6+5lm6b%4$maOnxG}BQ{=(-&Y5#Jp1KQs&u)1zg<ld9>
z+{}FI!vFnz3yRmz{xA4!vdC@i_>DU{Iy#+o4UhE9$i2$IcjHLa-}H)G?d{WF$6N~L
zJpZ&~9hW`ZricH!N)w;2*5_IqnBm3hwpbzEjMHZ?-}&=TU#9;5Vem?2dwtALp&nl=
zmh{DJ!8SixrYIF{omRT*-}lF#y{l?Y{C;{hZ$lf`_sxcf{$7$e^zdJoQmTd{YZ#B<
zWJRaYps$Tirm1~%+vE0yFS>E??h@6qSHC}mnwMSQJ^N*coYIS{R-g9YKOdd+adGmM
znP;^fZ+|><tS=`gUCQj)>w-t-ojg_#Edu|4+GYE*jB8_Kk9{X+=Vnc{GG6}eyK_Bu
zbw0`SoAY++Wi@T3qY{h^rn4q=YEJa(^fH^S)NU1%x=#Ge*F3TB3hnO-b_=v{T*zuZ
zm)@>wC01CZAtL0)<#*`$N|TGmF-P_vxtw*zE<7zad83_6tjY5iUCDf|m!4^){4Y9?
zaD4X0BWD<sk2M&|nlm2GJ@DW*V{`EV9TT6KIjSPTS!v%^rerHuoj=Jg+|X}QW1U)7
zKY2=I#DZI=xD2cVret4p^X%+0+p&Tpuzh2O&D8w<`f0brKA+9#KOLHUrPlZE?Xa_+
zKTB($Z_cxMeQa~y$^D*=ri~H*vz=t`&6_guZ;q6OrphC|85f`SHt(>p5Lendn|0!R
z2j&YCV{YV4t7c|n{$Bn1=t-%Q{$8qCt(G0!lP_y(FWqxeExo+UrS=T3&&vsK#l0N9
zEmNE9v({6q!FNW=!mJCdIYnQUiq>7-AJ=hBsOp{hJ=LJ1C%hT2icMZ6n1;4K+3S#1
z7NZw(DEOUys=&*$K3Z;_q6?NxDLP}N9_{P*M)aV+<dbj7I!T_#RSq67-Sx&xRo2Ec
z{&Dv?#VV`xiJ#xppHdO3aaCIXL}Bl0H=}?Mrw2Jp?my~y-_%(wx~RP+($6?;@5|rk
zOnoBOs+ojM{>s(Z&DD5Gl83c*Tly+B5kAc{ZH_rXA1}Fz$!D1cEIr(#svo*9#PmGl
z@#X7ho!02Nn0W4@*tAK3i;NUkG>NWopBCY!@-uASzsNKVTOGafc|vtb-QSw6+Ad$T
z$}>KZ_1<mae*W&G4j;e%ST*rf^$zXHM+zdtnhQ2DT|F22Dmz(er?pQ!lSr1e;%1B2
zAx;O*hWvbg?5aY_f8J=bAEggF#U$O#;`w@=wa*x=X?*#ntnxme^|r51cLXSl@HJQ{
zFKTmJHrXsX+tMI(+u1L%6VBY1oiBRa-*#tI>H@zPmz(~b=JXZwQa-tDn&)!s8BVkP
zwk~_Ioh>@!_AVY3&9sg8!fuzozjkYT)b_azuL~qT1(cq4bJ&(}qv_h+^-6kIk0}1x
z@cqcdc^!x4zE!*LX;11GlKMB}r$F|JzxOgXyt%e!Ny>v`YhpZ&%F>EdKBzRW+j2QF
zI)BM+v)6M^e%ZI7$!e0^S@*46uHJ$sqM}=PMI)16Nh^E2uvk7J_e-HK%PiLiZ<z$z
zEjG$4%~B{nw=YaBA@i1qfXIObtCMD0U0IdUTYBsIr0^AaPv$?dnN;7jg@5AxsPyix
ztu2dU6m(@*Y<|HY6XpCWh(G1r6CSzcJ#%NPZe4dSdRvA<cHz#-_+K2^CkoDZxfQS8
z`RtKScX8v9iOVMVGwOd?Jpau0YvS1lj1?NUm|H$S6yUSL^~2p|#&=7Nr`JRsl~`PI
z_|{i_^O;HiR|U?Uq-L4+p-uk^vuWY)x1s-T|6gl%^xBl2w_^5Q;hB=QT21na<>Jm(
zu2?_EI%c1@R?{x6IsE(V$L>uATw7AoYjs<iEF+JfSl4#QP(yT8eE;pGW%IAz?1^)o
zX%Z5oc$_Im)%#?2-<*_Br(W;+_%450+L_RH4d)b2#+ufwsh>}ZHarRm`?fsk*WC?8
zzx{-LR>{pw=z7ne8C6r##_Ms}$x|zTD<iMV>Z!}8EZS#sGCt_h^eyJwf<8{r5lPDA
zKGNH<jfG!PNi$x*?X~*l<BOln_nYX;ch8vpO5;;~?}IND|JlBmem^g6<L1XLdGC&;
zcNB(fKO2$ZzbyRSpERA7hwuJ7`|<aVPiJ%QpPTYm_;H?8*>g({)rEdXm~9PaE-R1Z
z75aAn7NcCrX*O~Gd7pJY|9W+w%b0&h+U`B}{9Ct}?V9&_L5QEE<EFI>G^@5W$Q5a&
nu$oQnD|k2a|C8KDXS~n;zpqwz@%9l*_W$DC{UJZi<rx?NX6S~7

diff --git a/examples/verifythis_2016_tree_traversal/why3shapes.gz b/examples/verifythis_2016_tree_traversal/why3shapes.gz
index 101702833ff142c7ec98d413680881cb2e439881..91299536654ca1d64f192069d6f4102e97ef8df1 100644
GIT binary patch
delta 5971
zcmeA${$n)3o$<*;j{x88sz3JM{rBZ_mwZt8*|Wb+oHgIM=KWXuJInXf?2kFMx;gyd
zrMdN2AMXx$9sBNmc)onz`!MhABH{C9Zx)GRh})}mJLvtZ$M^Lar@uS?H-6&Nx%Kz?
zwjQ0e@7CX^5{I%?KiF^heay=)^wI^TKvVv{jd$aWW_z>0cYSdGo58`V*M9#E`h^W=
zIJF+%_Unj%{N4$w8S14A&MrM{<?(OrN@jbn=dU*$TQx`c@}kPjt9rdzfmds57p~xl
zozkFStMOr}ipP?kiOXg@coa6j{QK(biu-rg|95HrZ~Fh#`)q@v(h6R&;_q9(TIych
zdgNNsk8}3-{&j06es(l|dT2$Y`qGjB9iF4-OdQ|8D1SCJ=^5kk>!0kWrTw4u{<ZvM
zSEhveZoQ0flUW+26YX3lb!rOq7#Zf~J_-N-;q?8T9nt^q+3#Cd|1^a0Wc-dRU)@E&
z?B4xj^ZwtO%iAKq$4iH95!Y_~wYxn3-W-kS`MS~Pr>-qe)$jXzDrHA_+pSp1@1h56
z(>~uhyX}M+SNQ7HY)k*W=YRicYW<G*pQ7gJUv})@w|94a?Vp*7#aG1=*PnXy?Sydo
zR_)r~o9oYH-<o>+xtqDE(cQoMroHBQ;%=V*M&R4A+Haj(cNUmtecbGyyXDy4g9lx&
zZBMnnYdUAId}Zw>9!rj5t-F_E78!?L`?vp(^FHaVMQ7z6?Rq)+`cu8I&sEJ^UmQKV
zVBgiGPj@CRFS{jnw)>`Nea5}j{r36W`)99y)_R-0Ps-<U#)Xb8?7ef%mX+Q$Q!7kV
z6l1j%S-kl4HMjHkn$7$gMK=W`s_Q@7zWVlW>;KO_z5V-G>)!pPw||u<^WP486YY@v
zLdRSyR_1SY^r1M9wD|aKvd{Ls{(JXK{&n7C1-~~r+n1c?fAfFmkt55C8CJK}mjy{N
zw*8G>&7~?Gva{y*g!10siI*m|@yvL%e))}z?9Z%bu`bN6l_7F-l&*LkeKfZtsMU$(
zU#9PUsUPPU_W%BzaP$sqpR}pbgxchF`|}K6y;;<IkX_!gY=b3duNha7=aGg>wxK=#
ziud(?Z+v50ZD6LRd!W51uvkZG%15K;3H3`2zxZsrUoy31&*Rrp)vJyPbo)kfD{g*n
zx35LO%VXsd8J^XF{ne9~UAEJHmm7Zn+YX%tZZW1g8Ar{f7oM4V(_?4y)6a=VXFR#U
z^0wK#YwxrKuWM?mOo|70*05+dCx1Ka7%DF7ci(7^!OAIfjo50h$b49};^z6Sm#kxV
zNDF>0sGr51dSuBb*+SXE;*Ma?+fTaBANgT)gio<uq=wgbi)GgLk|Qf$y7o;7l@3@f
zb>*Da&gN~+-<%z?mp(n9>cFUIAnAT-!oe0RwKTuh<O}!Cg|-~M*b{qo<~n1g+kb27
zo_OW6uR9|AbxnJrcHy0u@58RGePbLQc}9twQAwrq634rGkrt-)K`l9x{eG1^`Q;pb
z^LhA89jDtfE{d+~D&P9&$<5L)YA2br>`GUB*pr!er2g*JKkZ-Yr#OFVi45M-5Xg}j
zyJ*45T?^j6G+a7+tIzID`{h!X`}pkin)tLoqt&@9!ExdR&x6A30^c_UDhKvGoA@N+
zRI%5pzdv?*uATdDc~nS!bZ%U^NL{Q3&q0^`%`GaM#i#h3(3te#|LqwL^WR10naz5U
z@Ft-~%wUq{vMEp2dQ8xa{+7Q<Y0JFCmjUy?`Q*24Nb+<0#UT}HJ+Ypr_v^CF86mqD
zq^<JX+xoQBe0rYVc`Hvwxr;LrJZ=lPh@70HJ8uuyHFuxmYFpC6mCcnl`PXy&x~uU*
z-qxl+B{sZqo^#RO%*gAtep7R{A1k?gcF*je+f$!8E_BN5>TYTX3gPTFzmy~tbUMQ>
zNpF*}V|vp$mUv#_2?ZRARf1Fa4o-H}dLtYCRMe_EC-l(4n8v@g#jJC6tRhP`{aAGJ
z(IFR&L%*6lEfqJHX*6wJDp09kJkh^CjYH&e_pJ3>rwS}rSFt`>GU=tt=c5zPutq-X
z$Vs_0!&~p-)tT(Qd>Za6w^p5!;{M%YDz+{2$-C$F1--7zxA<kwy)@4uQ~V%{*R&#~
zsjic*9pB|>EZo`Q%5G!CwZ1*@$6f9-k1jYH`iNJpT(_*hwj?8@=jemjg%i59cWGQm
z(W#g8UALp*xmImZP@1yFU-zxP6}}k?;x36A&4EHn6T|cZbxy|Z+g*La?%$ikv!$5s
z-COH*n{&-}!TGt5*c^Xxi?^0@F)rzFbval*MW<K)n!(8=&PzR4_S{ahPC3S~X7#I-
zwKpFXRByfW=H=bU%&iaK{;RM4>-0o@s!ms~mDGhr^$kj%cU~Tk2w*DeH=K5V+xzm|
zvom(?{Pn+bf7;fw|H|*?#ZC)17B7r@kfu{mRmt@IP1w?$$Q_MGb7GEUoLGE4ZuX1f
zc?@OGU#`8&WA=DmQ-3^{|50~wO}6Jf{$i6RJBY2_cymd^@nt6y9_8`tJ+nV|@8X+P
z`B%)o%`*49<hlK3eNDsdJy%^fAN}v?)hMiY_}cT*%iX3Qy?2|;oEvPlaq+!t+kMKe
z@JpY%EyA|><&3nuPt1B5byxTQ(plDEVZ<t;e_o{J>b*?gOA<4?Jx|VlGpWFG(Z)BQ
zWbZTWoED}%|LoMGmB}yIuJXP*DkW0>*pBUxj7ht9pylx-ex=OEz7x&rdv<^KoFp!@
zc&F=u%H&@XlixhMa`t7niTbz6txoA&Cm!*3P1x*lv1+N$$%{*sAKq09^z#kBs=FpS
zV*3VRv1v&@fhqDlPg1zpqD9!97>ybiKGFaGQa<nR-B(6We@u{E-o8@wsD<*pY~x2a
zXKoAm%Kz==+xOpZ$RAqxS8>a#cJZY8`mCJ#AD`a%O9qKGJ^Me$|6&HuA(bgCfv(bh
zs(+a_Z|%#A-CO>8?`^@?Tnv0SR?I1N%UZa0(@_!cX+1sLc0~UFcwkz@|1B@JUC&*A
z`yTs^xQ{nQw4#a`rZ4X8kShIPC^C6s^^VQK-W{g7=1!tNE4=ofdTqd{*(a{u<MPH$
zSh_y@e})-nX14H-xWtROe|GM@-h4&v&E9P*eFOFiNXz>#eaJn>OZ(8XIi`gVJp8=0
zi!WT7*q{><TWDxM+cM()#FuCCzTJJZ`)2*cH2#w=%Qvo=lyXTmsYGr{v77O|rzwS3
zOL)TidhVWCEaTh#=@k1bfu|W!tN$|0_<UB{(VUqly?%Z~_ng&*LN87%u=B8tms~5G
zeJqRj_{6x=0m4g^Wff%8`xT@-(;cd;dk%%Q72MtVHMQ`y&yAMc8!huKb9OaIED{K0
zUzpRO(8=WfNR@MWuwLRTi8tzbDX|&V7KN8R7f*Im?-h5E5<jH=P_u$t(jhw1LnD8q
zgwah-Z~qw;tLjTWCTA-s`1{#x?9KW4bm_--n;WMO{ZYJqRwt<B--|yVd;Tb<rzxgd
zb8F5|7W<@R=q#YQSf^rrlhMVhUL{uHsX@<fTr^nG&wFWqg4l~Vm-NQ`Q{6YhejLj5
za-7tVGWDc@YQzL1R|Vm$s5QpIwbFhLwvrQH$y~BrQhb8@;e_sbow<cKE7Q9#CG_^6
zt6IF6FL1TdNi|FL__B<YudB5G{Co6RpZC`to?lO{$(hX;TIZ&AB}Xsj_p{9}vMrqs
z$^42l5cRZlb`9F5x9m;Gm6b1cu6V(8z$&|&pD*cxCtLT??D>q!UVV;zKIyxHFVCE7
zVwG8Pslswep<-u@nps@3LcL_7?2|W34xLGCS2OipX}WmQHJg5k1v0WbV>wfvoyc7o
zZT+7i@<eWvz|Skn+n-L5ahYdX6#Z(c3A^}ACg1Fat6u%m3A)KuPqu}yvuT`vk~DF*
z^7h$bVUMRj+BNxOy3*sF2|?QqE~%+J_@tGs$b-$eMab*aO%^3(MU^d2x@|Yrub#E=
zrc&3mtcy1nZ+1`bpMG3U+%8LYk@leo=?Tuf`7DuMs!b+chgy_oO=A0Xv&l=}svaCK
zpME@65-$nxXzMwb^}2=UU~7<4lw?fj@jD&4x6b=Xfqc3r<I)Zf)t4f*VwPE~$1=~h
zFfti$^cOrC|LlHJ-R@`Y=E?gq>VurZz8ngDDeyZ+z<R-Ku8o{`YcvI3J5PzfEAW&>
zPyASffSNVuMHfdUX?{D0zMIoe2%ebiu_%d;ebS2q6@mvM&hM2kDSwu*^?3J<X;;gF
zOQWY%SKi*V#`s8KV~CdZwwy0oOspsC93I#oF1hn@%k22g$)%Hj*{WTgEU`ys@~X)C
zz^%G^nwqhEstH0}OuGa&En_+^v?NG6wAoTVw7mHBvukI4CHfCZiE2pbw{|(r2=P~X
zJ|k?0iS5B}FF3?+xNbk1*L_#ae%Wj1lAUR%H$@&@w3k;YYG#+8AIGA_vGeWB|J>=_
zES+wCuHV?Nh)<V`wQ;xG`;&sNI5xE`I=L%hUcJeZ!(66^JI)n*)XF3r_U75Jal$8$
zfF^;HR#OjNS>rC@drIKJiMS(YSwey{KW@AtGiT$3lMyLye5-Z@Ec)uX>04^UOGTsN
z)ZABFezZ*Wkz3lM<aEmIS%}ZFHOlS&jXwnE>)*d~fB)V+dvCw{yl?OBSkvaNsx+U%
z!_G;c6TcTMu1__NO>4V#wnRDU|JI~WKWDA-z8ETRnC=twbk2q2O2*r*ExL+*Z8KhM
zTOR1E+J2Z>@@f3al#sAfSMUD4d86u0pO;yu!inhh##59%8KecTB!7R!@c!&KnWJt3
z?{+-d;V$oDZsj7lqcncGg7VFlRSSyjIJ9feOtO^U)O|`Q)pUQoY2uBU8=^`s%8BRp
ztynAg#B0OO3gxMb4?J1dbVVm>`^I~jR$Z4Y+Siu2tyWl7lOE>SAlLc%<-LdRQrs(E
zX?46^*;kMzdgMpLg}1J59@e^%#t-L3um+x<v975hao(ma>+a3edLQO!vNpz_?Ru!d
zeX}sZZtVjytJbV2l&n;g*j9h?lejRmZ?#lf>+wGy{Ovg}PTRJ4`{M7L7hm^&7~-{5
zLB;v#ik!WncP1~LU{d+j<jX2yq082tTbHYr?<wE&U-4eP(Y7ZN!K&F0JTx{qD>igp
zZgeg$Hu8TavE2M}qV6@hn6>*V1+Dv<C#U;Ium^KAU6<*pP6!H|x%B;WVcu0y^)6ed
z>3z9B^?#^pK&vXx#win8&7(H(>w2bz_ssOWEVJ&`#od>lUHkIF(K_~zyMezLL(4?Y
zW}~BAF3FqEom<=?aP()X+@h)90!2$$|K8j3!iwWtddm`)sOHa3iDI0Fs@a=n&NHal
z;u&flTRp$lL_fI0PP}hxi_f{J(}w%~BXa74wy9X1&f6gVpa1>}p3PoeMO<!40+HS#
zmfVy2mgsnOzdU#--GQ&z;9bx@gSbj2?^`atajEZEH)JSxU3rsmYvq*w&pdOU&Ro}|
z9Bg>+b%v*)pqT5$X-YAUtM^=Ss@xH?Z<o$@{^|YN^7WN}D}Jy4Gi$2Ro+tPBfB*g3
zTkz<ktMza6?=1hlfA8+yyZ8Ri{Q2+itG_`pdslspx_{_vm=0UatNn3%wf^aUUw!rO
z`s#@Vq2K$({>y(a|Fg_9v%5BNo7zLMt-T+@`EKMIOk|P}SJF^UGMd3veM`wrKj_Z3
zcmHzN9raztx?kEf$(sA$@^6pI&L7+V)BNAV<$tX1-`)Sav$_6b>FV|0t_t0;JL&r8
zz}0w@U-z~-Z)~ai`*f4dk9gzz9H)P-`1;ni`sdGwg__q3xAni5Tjln&sBXDS@o%dM
z_wU>Psos0q{Emv<-MglY7xtO7eSSA@`{B0r&BwI<-~WC`V#huXkrbn^ESUl-OPX|A
zI91iAa|`~iZWenq`}grxt!vqSL_5Cz#y?qHNVop^{P(PrPpP@?iQl_YS>@b*S-Wul
z*M?&IHvA2eZ+Ix&?tgMe*!d_MadVM9|3d!k)SY*`cyG4ae`oHnqME-G?q8XCeW}$2
z)3+sSIT!V6W-o30$+Ed=$)bmOlQoYz+<f`#UtVeT_q^niP-}a>UAy+~of|ww>aXFd
z1G~JkP0wciI5YXMkVbv{_U&60VlI7^dmVT-RPO1^w#72$e}11lY@D+_TEoP>{B@}I
z=Jh-F{SwG?v~kwUKFHtUyyvD;&HhPAdj(FcJI??0o#^Z0x^i*(`>n@qq%1eSW>xsP
zJ@oGR;P<8Gzvq{~-(h*-lyC6&+28iv-R_&6w#CC*da>-(7aYNt&6wlZF4vniXU@KR
zy6nA_&uyMFi4jfGm(6se3a%Ycnb+2RM7Ut01-tm1_p<so)_aJBas<xskqMGoUNcc<
zmPV%R)6?bU{5LndwwPaKO?he7U3cYxa5rcEhqK?ah38~>7%$BE)|yvd_jd03j>ESW
zKD#vQ;<i~2=Y4b#v)I79TinBtd#+}5eZOYGjDX_zD<7yTR%o6#SrYc&JA>`Ig^;_=
zO{WkeL9cAjCk;*tuU~k4dbm<CCx-Le-c{Ub?3eFGpJcdq&81JW?bhw1LB?hCb(9Z0
zc4D%aA{76d!BA6U66?{DY|$5wn!Jxr)tP)<a%%DPe;*C)LnQZBZM|hN>FM8d8Rhlw
zZ?3XS{d{+Rb+X*~1v$NSHqRC=mYBBpX4{!NS08TO<@adw3x|0Z7|*?6us`#NiG%%|
zV#h2WrZt-kjh9P)Gdw9H*D-mSh%?g(&dIMu)R>ktOcoZ^uh(~9tWoh!BdcRpLC4}J
zA0ij8NSp8``*@diqo{SW=x@ac&!babEa_?d@2@6Oc3wjJWb=2=%S%q%^BlWcmg{`{
z!uD=ORmbe<tc}|zIdJr?SIlBJYxHSf_b=^*`}&K)bC0{Shp}Jd*`S~z$T7)KVWov)
zgGcqjzcWwCeOW0H^louI|88Md<98m`A4(%?D>pb5GKJ-_g}rNbyQpJ*rg3V+B<5Im
zwa8vEuh^Q0xkAg`FKTUh^YFm;g}3i~y#CSr{e1Djy*i8cI;JlPv8v=TWO=>x#Gy0!
z?_~T>=ve7l>&=&*9;h8({=F)(sN<IQQ_Ytmo377FK4Glv{_e;Y;hg1b{@0t#yllTw
z<FFi`+K#&kPVDclv&LBP#fY>Yc$zJ5#1^)R^IB7hmX-UVt~E->)}#m;?s)lX%g#cb
z@-&_`&AXd__cNNiThA0Y=_R1b(bg&2cXOsJd%VXp^}c7dU8#cS`KAk>R*GUs*j(}H
zbo1fmy`9e2A~mvICQVUsd$~z`p@ejO(UB*Y-1%;l&e+2<gG1%zWY$kS5-VdS&1#NY
z-OGJ#hLLT;r^sVZtjglp%4{Zc7no?>_}d@3*u+$J<uxng8FLzz^Y4~j_ucx@$&wd)
zdIXHD9__f8p%LjdchW?!=N@l9R0Qr`?QgK<n&G$JM4w-~7>~L5_GqnPUoD=dp`dx;
z)`I%S=`wb&Z~VTtLEQ3_SEG)md(hS9FH;Uo*c<4US)NyTHC@*A#e+Ye4*c|V=klm_
zc^(pCx^>1z$)dg{OC!x9GoSO_{~om;v})LI%23=eYtH#8U4^YP!%|8jd^nf%v~P;v
z{(twk#H~qT%7*nfo&Im({^~0x5a=B_NyIC1gV^S?^<qMoJ!bN0)Si%fpYQECzbw%F
zw~XBnjS~yY&b(Ec?C^3=a&w~j6Up#r<!fzcU#ls2aN*>v+s;1~_OLz-KD*NS!Is%4
z<Gx5<i>;6T^>+#P+Ns5=mT3<jOww#SAiT5bP4z-2alS9re*N=v-_{;KusKnI_4TH$
z7Xy`)mNGF~N@|ML%Xgh)FFs$q`=R@z->Y1Hdu}h>wQFjtq_Ns6xdq#mj=f3glF4xv
z`ux0U&I#9ogxJ_$>P!07GTSy4HaUo`-1Awkq~lyv^3*f8{|K1+pSwRZKF>e(ujO>j
z^n~?~BkTMAo^raO&bQ*<xq{4Dxq>ObQ-sA=DO%oKeKqRE)4!KuOz+p{e}B}tG-}bh
z^qXOfrZ@d|cJ{wkF1UWY-%K*1-O=UBV&||n!(&k)#ZTU^bGo6@c+~9T%Wqr0#^#vX
z{V$&rbf`z@(VKTa?Yb`VZ<am%@bG7)9s8<^Zd4@g<4S+Fdc(Q!tHSf5SNLfsO~0&T
zyEW^r-bP2`k{Dx?)sj|=B(qG5@A_sXar%nfzqj@D$Io}?-~K#dq1yS3`dQW{JMV>T
zf7vW)o*Db*m+-6>+1ra-^4fHE7GG`r`Kn>H`}H|1&;43fYB&3BzW9Is)7l$eNeePE
F001|8szd+)

delta 5983
zcmexk)L}fqopH@Xj{x6z?+^96|Gs=KYQJRNtl3{D&dx82y#Km>hkxbIx}8(P+1EEM
zwf?{Ac=^I>yYJjzf6wmDy|vTwG}qafr)%zD*i#j{ZRx$M$M?rG>D}%Boj>vE-1>Ui
ztZviVt-qg19LiSxV87va_tctIOBT8=%94{w-n}=)Y&ze)?gRVZCN_P&HuqnmoO+T$
zD_4K+*G@&dDn;)Ley<#6d$*TP_!Aw>UN`03^~By#OZ8>0pD(S7mAblU)$d<Ufr7g<
z7#*tu9(a3B@Q_sYH9UB9t=;=~;p?62ivRy}VgH}~Z|eQ)2~S>qkkWbfF8g(H)S~Rp
zwNF3Ht>5!kJowPF=Co6-ft&rjUM`4`=$f0^bnoK(GulVbF!!y0TCa2VpX&YV`jcIm
z66z&$wj8^yBs5iF$wk*=Z(0;IRdaHmg#Z6=`u@(2=>PZZ_pQ5Mw5s8W{f;YN-9^9b
z-u+|q{@<F*+akZ$o2|;w4`cdT{{G$`%fM}R(c9)}N54N6C-Zyi$%6GfTX!41({89f
z^K9qr+=;p(>%zi$z5d>pzxP!8f5HAw+Ii<*6xP>Pm)HOPVeI^Dm2T4dGa8F-)c)L8
z7kx)g^VPa<8}sYG^;e!fUKIV{#WJ@WyYF9Tn!mC2;#q0t*1cEf*Cyq<$Mi=1c@r#M
zT4Y{WFtIV=W<$A9;&zX?`8v*gLG!xynoNJ;Gj;2K{r?l*yRD76+_fXm>UHVP?yGy8
z5_PKzjbD^*once{q<*C=kIUzzZ-TSFzj}QB_S?tLR#iUy*0^}ul?nxuq|c7Y?O|n!
ziejvmB8wNFzUFrRU$dECqv)o9M05RT+gIQIZT<h*r?-C}Yu&rQ^!Bg48#{7KzlSb0
zbekr9SGTY3{<IC#+irR{uWgTfUsZ2ze5aII?asb87liK`u~awcoeU}At54W^!Ou(i
zz=rnh(1j_@TGR98KdmdY_ldf6fpPMmuOckDx%&<*>&{r9(SNErxFu?3#2(?mRRJ9b
z?AN}G_P!T+tGr(B%v9@xg^S&$ZOA|K^}4Rx+}JIKKOQK%^P8zJyy)hr*C`ROYkAj4
zO`Y4R_S5!W&&ctKYT%b#{4B#n<8f;Jxr1KGFJ`9fe<}R3g8#bdw~$^%vDur%oYKzE
zt>jdkG9k#*QX*`z+;=tK_cdX6ZrkmB8x`r$yCdttg|2)vx0%|TCl(z)_55&`;mL)Z
zx7eqP>{dTGWsR>Fi&InaPmVA){x|K-tMshq>`S#s4AQht<@vQj*;CZ?_s+1Y<=o}U
zN%eAm#fIH8LiQ=IQ_kZn)XJP)^Kqs`eA^AhCli|1FYGjPe><<w!gTM6g&VSz(?b_u
zk5nzcP<Ek?BV+9rnH?+|3M^`mJ*13g1ROtdW@Q1-t=l`hHdxGZTxE5=)GcNA{PX;Q
zFW+)ZtynbgtAT@RpY`9nr*=)PP1Ej<Oi^@bQ3;f)KRCB3;6Z5DgxpJ>^ZR1zUugaQ
zqczzzL)v(kQs~EZ)8^ak?z^WF>2P#8pXfaEv%Npo@1FI4!oU6^k9h{!U1A1Yifg<@
zOd`d%*xD{D**q;X{M+@#Z>Dr=hHGy6Be=G}Lr_OU$V#)~5yPW6vn-WU7h5LEcvt#)
zZk4w;uikq3e@K0I*6Opb`wp$=ZdIJ|B6r$^ly6OwI3-<${?tngzqo9B`mCF<Y>#Zu
zc_ufbqf;jB5#=;WJ^jx&tmT@qj_j+;^Io162s?AqL*8+5R{ER%g&Xgci1lWPU-7xR
za{Goo@19*c`!rHr^MJCHFi)m*Q-@OIrlXU?5B}<Sd86gpo2n;nF7@9y9rsJK{$1Su
zeBzqdRu_sr)|u<RK6QTOq_@{*tlK@a-1z^tGd3C_8oq^r0s&oGi67mfe4Mf*&$^#+
zEmM2pb7AI#)rm|(e2OmmO_vlaHhHw}O<ujnDZPKKm&FY24g2%gEtu@8-t8wAZxR_Z
zgTpl<-au15<r<&shHWBB?^E^aKb_=hOsWd}ymgz<qc1Hf>NEX}=BDhkn6y*jw9Ld_
zAF1M#s=KT{FSy9~RAXzHe`Ipv{0+wrnf2cJ`-gqq#urnrX|4^vC9LsQX@<keAipJ>
zJTCpx2yXOIQ4*8=a6)5`oZG{4eS>ai{-Xx5FP83_W%upk!azf@=JHl2y>%}ZIZUqK
zm}0W?5!1ZYUpzf$_AdA$f7R@v>B7bsf!2jQZk`=3Q9E5Ws#O1c_fGNmkInq~SsWGB
z+qH7lH{A26+14q|@=`xW<enzW1SK&+*872*O!h?_R_RvtFb?{hxA^S@Y32><R!!cT
z)_s`wTG8g!<>^bWwr!VWc=MHe;{1?J8rxoGIMjDDb*U6Cmrr)&JYjn*qVD#-`&&(u
zpFMl^|M}lpSIw*+l<uyKj5`~1q_T1L#se>(a^Be-J#|y+LpHI^g@TI}`{Sx}7oD$U
zx-ob8_A=ueJ-fN=>NIUc<ztsf%rUl$^zdVf+;S{!GLzhFwdT&<wmWA0x2SgCT)Qvu
z_Koa&7M|*N>(f3n=6wzmKdbg%U6a*s2T%0;>%RKeuIRtLlv3vR^2oKy==(-Dt?b{(
z<WH73qn0wObn<N%wk>PyUTvPi^yq|0z#f}mfw1c3rk=?udTOfqo4gM_?KrmSba@T;
zlc=b*HD=*r&wCe2hnTMr&knfL`&)ve_=1d{>r<I-+m0o@=C1X(4Bp*S&x|YRc_zmA
zy!U0Y&!*YI=F9aj&AH((#x++{q1#-;>70`5>#0Vn?$i5P%4hdjm?nm9-;kGh_mE#i
zM3<rK#9D(1lQkuB0%bT@Pq4I2+W%*H{f@8Yt4~jP?3^}7PAy#I@tlfvXFJo=Zv|bo
zzmdLu|NZ28j`nZu7gou|)pz_|x$*DA)0^#6Jt8?~{V%q2U2MoPIY7uoG}mI<7w$9H
ztag=ty|?yzp8FbY28)EnMb{)(wr)Em7OWF#WOVCM+TY{M(Mf+VFS;GKeQ#d1d_win
z^xzd4XBlJq%#^aO96TQ2<M!_1IX_*+Ye(*Kgg$w!`B!WGVV}hoacc~OHcI=}=dAg=
z_~x8_YkeP7wYqNq`21TOf6(j=-)}85bNuR*Q)4r=O}{{EEywKQYeyQDEj8DkarAa)
z+7wWF^yr_QX9;`Vml^NAS-$yw+JD#CwkpDNk1g_=<T<_LVr9TN$+H#HCm#*HY#3o_
zRA$^?WTJaYTYiP}l*O5AzcDAAGtXza%VSVKr#4BqXx%Z-1<K986t>r-ZYf(Mx!P35
zy-L^FcS2uDL&+T5mJF4-j4$6Ba79ZVDt&%!`q8z<iNf0wh3lSec*&I1;p8IQvPrQ?
zg-fP$y2>2Coh>VqH_YELv2@|vhev$Xd;O&5n#2iY#&FDUS^hvbg&{Xpap9h$Nhea&
zb!-zK)vvsCw0~`5gN^0KBW9bPPM>~E{!@ZJ_viK;^UWR?e=h!f-1t-boSCgt-s&u=
z>5DwkeT2txNzbMSd$~@zyf*C;@d@#one2Xeft{Jh|E9<V)q-<b_i5@UML*<TuF2}j
zG$~Zgc}jxgDUn8>6`32)`FzQ>VEmfmvZ~nQ`Gj+d`Yq1&dYej)r9Pjl>(y*(XZ5<b
z&&p-(DV5nz=G5F=IPvQ0bsv6r_wP4(QEdETa&+~L8m}EvGXpm7EO<Nn{G#<wIXH`7
zR38jcdCDW|d2`o{O~HZ77d>CJh@0W{8eKb!4o7uK9kKPbY&{y5Y?elIU;6o`mtA_X
z<f7-}rxT8~suaz<QPEr9n9@=@Ve@1z<969uS4@^(>+y>EY?IVbRI;s1b;8WeTbJg&
z{llE1xSiAKN$~k=)0~S0Dxc-#uAF{JCMJc;WG!QuwryU+)}EI)Zw1LpEU=l}?fUNA
zwY;dv-uSN9e#ho__B?O$yva8C(^J;T;!-CRCC><WX=tVkcl5MOxG+ioTm6Z3S#4?E
z8d0lU)BDfK&9#k_tB(1xqO@ZjM{=$MpXnaK6wRp|mo&J9yE43_UZitt?S1hF951II
z_jku!a8#5uvRb`X*oZ~kt1~0DKvk|-d0VEvb!N$>7fU`a@_ei`bxH7-$R{gAC6=2C
zvvHg`V&|$-KeN93=i6EG_j-QTFY@G!yvQBC)cH-Z<C}&&ts`nBpO-qU;Sa1Ub)F);
zBSs?GamE`J7h%@U9Gf2umTB=y?h5`&on4kP9*dYCyD}u(ey_W5cV_cdIsK&Qu-m>@
zb0gn9%{{&8oWOC`pp|cKY`VCbLqz2_W8?m|mpdM3n(t3L{z~m@wa+Sb!wO5a(E81b
zvZ7;xf_BMx9Z(TrEm2JIW$jb-SZcP4t=MkWyJy$VuAM#GK(5tPE5IO*OSIKs<vf>j
zhHDEltD4?k6x7?$o!5O=Y`1Qm&-L~fMQ5j_ZtilemUh`<BszDFfQ$QXyV|@TJEhaj
z&*jaLPoMKdCQ5{hsl4~zWaTS@DV(m8OAprDWO}rVX0-{<eLmrr#eufz5(&wQPbV&5
zQJhq&)x0vY-(c1h#RC)fcFg8nvFy^L<dv2d$%>OVp6HPYDO~9CdUDF!(+roLQ=Xl=
zbtUs7r}j)6FG<&yDZOV_&hUwJ=bO*;QQ0nj-_HH@)s@xT?>?`sF5jKSCi?Zvj7M$l
zN1h#i_psjWblR>nJX>eKbUX6zeAmh6*{k$i!)uSsG4z~T>?GfP=FYnZ8s|*EE?9Vb
zo}1}Z89x4$DfLSy1x9Lymw!)Be!bCJ>!wPRLjK-!0evcrIW7VHcULp-F~40bBJH^2
z@ubIcwE}lv2)I7DRy((;Cq;Nw)2W{dYrYtIKdU*Rr{z86YW<&UEs5!evM#z-znZ|f
z^hBh9+4aqjg~S{MxEFbGZS|LaJ$Kn+iMUU)#&`U9?$^feH;qfy-gfa*ht`joPX!ma
z7uD^$y~FyG;JjTnN!53h=S0dG+F6!VPh5EUT=+GSo$AxvuNW;mt(-99fX-U}ie;yE
zKNa-VzP|ZLY2}gayh%qM)pHr_)Y8s6;1<^*l(XqiduQXaSb@t&lk0vgpMNCJ`}W1#
z7k}Tp_<Cu9*3uw>Neh!gw%yZu_bA9?)}AV<s;iuxFXtY)l|04zp7p)|0^2Plql<c0
zPBJa%5HXp^pykKj_wwvXmRZSj?)e<w9Z_Ad_181kGkmi9+hS8>eH1z3il@A*Z}fCc
zowjfOd50BQf>)z<U8oOFikRvkI?dqsdDWDMy<#UG%Ab7GWqA4L?88rOs={yGNs_nC
zSl<1g<Jn231_PtSfMpSl89CQ(R*DENve?hyvgMN9s-|@d?$6ebWk2|@XTlVR?1DIr
zGfIlfQhd!WFK+KQTls2P_WRBJpHsOmK0j2yaoU8Fk=en0c8ME3Z%%rlv-@D&AN!ic
zMrX7%PiabYI;Q9bKGE^8nzTtncbPihd`8PN2X}b?JXG<NQzui{v})>3@dJx`HG(!b
zXD$!2J7-)lEqxbP-<gXQ>ldrKx<rV$Mt2pkuKg6m{q$kc&sUr7*vHtdtNHWv>*Kfk
zKV^rV`cOZq{{OxA>-AsHc(nRv{0{%`_0{F&<<;LWfBO6T>hGmHszP6H-PihhZ3NGb
zEA@M;LjT0S3t#;^{=3q{Rqy0=|JlEL|HF6kC9&U!a?YO9&60k&US`AX1SM7jJ(mEt
zBPj-=-?q5+#4Xv8d-w0{nC{tU#Outnj+9mX@qc^tZCYRb=luFVhy8z+?%Q4eU6}px
z>#+E@t5tW@PU`;AxO#uam%X{|Nt}OwoldR%us>~|;Iz+yuWwg>`}Fzn<DhkqbL8*a
zhV-6#`bVtm*|$=K{rl^Ge6O0`vEyXNuHD&83u-fYp5L|2Z=ajM-W&RF|NEVW1+{`2
zCsJNryrkga!5YaS?B$~;t|a*FJDcti^Y8tk+|eJmH(h%xKAA^Iw_bhOd)CRP)XMk7
z?_H^^a&Et@T{!=1L$Q4u{w}s-IIPY$e^TMvd0Q*=@-!;`uKZCPZL|G()pehL?P6=5
z{P?A~e`W9{@6rX?w_ZjGyGRFL^J4zYna1krdibtda987|%U}QAef90#-D59SmDS0V
zlvY<;FV`^rWwh$RF0X9UvspjROx_`+QD2{zpY6C~$!ptdi)XF2Idz%W-7@dT_sQ+)
zH}bYOW%Rwfb~-XGzOeSI;+>|7wwP;8@&fG@n_Yj@bsnv1oe<kE|LU&xHFk#gdUpG`
z`zuX~lCEnzf68CI>*Dfzuk*gyzrR;lykP3=W$(=2*6!YKwsz)4rMEdfWg&}{eSB~8
zR7m>N-{x7CTc&?|Z?-|Mu|azxXP(dPEg1(RnI~6B=?VECaD5~bQ?RdmPr`ns$Ph)B
zM598F%sHQ2i!v51DV?H!|E_Jyc`?CzA>tF3-d@8N#O$x5w&$Sv{q?>Ds}#?+Y`ST%
z>#oqY@_kBt-CeW1v)yiIwN)Quj(l*y>`k1)QJs=yIrX;74kSAHo?6~Cz2(7Do68fT
z{^~E3jCt%K^D%`x@T7~zTGffnT#aiMD@S%NZ`)9)dgJ>ly&1AT<@u`2716?$X%boa
z;@)R()Nblw=;!8q5a3nwmifq%1s-A|m)C|a=;qcF4d3JwmmYF1_Sf;_e*#j!yt<n8
z*kjsv>&16#?{5yZJN<0;`s!r4^9yo%>ujDaTr6?z@XfX}cdkC%x~t*Q<`)k0E-;>Z
z!C-&p5fcadImM1ysZ47&85%E_{APGkX5N&^vqhYlJj5nH5K&`#&Ni7tRKMQ7&n@u7
zoxm#srVj<&Pd?o27I;?S=Jh_&awhFEHtlcD8zyyWUi6e?{y*PG<IOz7uu1IiCol7y
zUN6zJ`t7Z@zJ>YX&R$K|^thSwRT~9l;+?PX<uJ|Ui~W1{LVw)i<yQUOd~5jDNG3RX
zC<&+}I|LOvF--i{^xJr<?TcW;C3oEG<;&E&((X(wd+>V0uTKfBk66~+;aPKsy?0S$
z*$ifFMpgD*eLkC{bf@h4ap<;+U;m=ejGKoW-#c&L`FQ=~{CoELi>e~ss+-SwtStE?
zk;HM$dt&R%`(G{RO^7UsDT}c)*IOL6FYou)Lr(;@hMx+)q?xkb^!S8yx4t`_nd&$E
zBLCNC8ZEC+3T(5L@hRASu!Zl=dhQ(sGCMT*8c$!hOW|3QBD{w6Wk^Y1i)f^4Pvl9Z
zq=L&=Gm9TbygMTi!Cub(U7k6wugpks(o_X60Ulv(na#%5eETMx@s~OKTjaFTJXt;U
zX|7us4y1j2GM&BMUs||*&E|k>9V(ihJ(p7Toea(DpLCpD+Ap)=wLzt%fuP4Fb?zsU
z20=SjOxgE_NsF&BOs)F#WOL8S(l>i}-c+cGKgbB#@LPVfTV~e0ptYrG29}Ke@@3XB
z@5_%&etDr%QZc3ENa5m(0h^{+sVYxBH}S^9kBiE}=O<*WO@1SNc*d7f=AO=35}^_P
zG5Ti$9D){Xb*w*r-lFE(#_wwr^^2ZNWr_^yTe3?1jb@`__2QmO@9sQWb>6D$!oi<U
z8$VC(6PfU><J`&>Hs5z2OFLo7_3T8*<%z8?9WTZIF^FLQu$?V|FJSWLnL&o@3@&%|
z@O5i8PWc${?e(|%>vn6x&Sa@P(~o{Jzii>YlT1okn%<L~G`X)OZL7cOlq98jnQ<w9
z<m11&nlCTwy-J&Zm|dRL@=D*%*c2g+x#c+qZ`y1gpZc?IYx?C`{CqN2k;T;-@-5pH
zYF1g6a?B|+zS(Vec-QNE@BQ;j7H%zCr*fP}CdTNfK!sBHgj)TO7l#__&cFP)dF|f!
z5*21VOA=zYnOS+cED2FiP**-$|H%2`&xCiCdFFpSYT~D6*uOOM3*WxUAo-ZfRpu{Y
zM`q0Rnb@4`k@WAt1mT?=d}~&F|8MznQRQranV-N3rK#ojn)xn9X0Mr4Ia_|wvy(rq
zKc9ZPa*h3Sqo+J?N^M@B-xwds@%sql)%%iqzMFNMa^~keaxzs>uihHPy?0Oitkuuz
z-{0O_k+5>wir0$ULmhm#1?N3_{43|q*PTmz*{&rD2!4I>Woly2MzO1NSof?JF!M~<
z=v%VOwyjn?x|g3#Zuu00#Vr=QtM~OMeL0+Syy(Y=Jsj)S&yz8mH)H*wnLoAGd=CBk
z;<?zW%Uw5~nt1!KjoR&<bAd<pI?vgxw!VzEsIxJC+h;{M2_M~F{<i2(&G+Zu7No2=
zX?$z`Gr!<<=2vrnB^>jO65su=MJ@68x1NQw6}{iZlqT%6dhlwdS^BEY`!eUAPy2oQ
P=znGoImHWRf{Y9Ro~WM}

diff --git a/examples/vstte12_tree_reconstruction/why3session.xml b/examples/vstte12_tree_reconstruction/why3session.xml
index d79cafc89..9c702e2b5 100644
--- a/examples/vstte12_tree_reconstruction/why3session.xml
+++ b/examples/vstte12_tree_reconstruction/why3session.xml
@@ -49,7 +49,7 @@
   <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
   </goal>
   <goal name="VC build_rec.3" expl="variant decrease" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
   </goal>
   <goal name="VC build_rec.4" expl="variant decrease" proved="true">
   <proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>
diff --git a/examples/vstte12_tree_reconstruction/why3shapes.gz b/examples/vstte12_tree_reconstruction/why3shapes.gz
index cb0ae7766119174c73a087be83079cf6dce02fb7..59310f1712bea86dd7117ddc2c46d9b3e9a63037 100644
GIT binary patch
literal 3442
zcmb2|=3oGW|8HY*^Y6Iv{d*Vx@VvN;!IJ_DV~1b`gFHrN*I!Q;tUtPE8C#Lxxx!iZ
z_S^TB?VS{M>D{f$)wh`%b2Fc}K5_n}=zeR*gd48grcN@Rr>rXPD4E=RN`Naqu66e9
zs?Wcl_Ul`}QHa^Q`|pL?RS&<Oy*=Ud@89wEB^OqnZ7sKqbXyV9yR>7Lt#hfKMvs;A
zu02-y3qJ&NmYPhl-fVK^#D&)v4X)o@nz-%q<irJ5`%TW3Z{b{j|LLVtU&%wWxL&X<
z;B*drGBsvn=t_&H%JF64)4$%m`?TzvzI=ZEzuz0*lvUn**%$X#KZN~yc=-3|t=p>m
zTIw$326TT<^3f^Wpw+>8^<UBV-$%O>B_$V3&s%*`OX1p$ymAex7pymH^e1_26BdkH
zo5{AvKsLj5JF8=$?&<d~bvM`e-e29Qa=2bjZ)?oE@?CQ8lG_b}?v*F>&$@7W%F^H4
z)*1^pr5^I=Fss);;;${GcQ;>aT|-mZ$yMJ3rv6<etF|NVs=#hl>F#7totTPvUahCh
zOFiU-XFpo4(te_~S+(Bs#>T^6Z4*-YuYN0V3lG(9U$N#1*K21JJr-Hsn-9)TsIp6*
ztm(0>`1R=<>r~qh?_TG+;mNGR3kM7n7bF^qyEAQaJy4;z^O-WYr(VW`bMK0Gzd!cU
ztGa}7wW93eh9|Pd8-k9w_N=anWXv|We<E!*ci*n_rFuIen627^SZ1_1vAb#(Pxxb3
z)APN2Y0sW5m#^>MvSGjFH;;p_9KVELE;Ls5S$5XP@aGoSvwqxn&mImInlHQP^68}C
zAzQ?sT`<^m?#!>Z^Nu|ExI)T%(@u?p$0y~m#5eeyv<lm{@|94qr&_O*r%mn&|Fb>q
zLJt{2_m^~8iWWWCkg$m7YI{&)w_c>9*GtA#KR!Oo{r7a;lGWE&H?7{bSm)N2-8(JK
z{1$l}i(Sv3Xt+T_#%z6`F7uW40~=dgS{JZ3x|~m&vU7UM^m>C+Uxk*`rJR;MrCWB_
zg5~+oy}6pNe*Ueqe^dA0_|L5Bdsin*H{bvB!D!{w{<ya7Prsf0yI$$nVfi1Q>;C>-
z`!{~Fs(c<_W^C`JUrnYJvloY%OyGK)^HV)qZu9?XO=s#jN?)y5o|v5ZaqHc4xqqhJ
z*kzZbr4+n^W6s_WP9OO;AL$Dh%XTY`tn=S=<?Qa;AHIG1yPN;}%e%SzGOsVcTb*O^
zvE(MtmNk)EuIU_=&0bn6Fl(~QEE$*RdD|pQ)3)5?*DX43{e4%L!|b!I7X??DHCpbD
zVzyrD{B44X$Fzcr{@-nQo8(*@bAJ8e5e#vdyYpkg2bI)ruZ$fkT%9*qR!raDx_fp(
zwZ5kP-KifI>R5}}UfkHmQn2la2IqNC&%S%F9ga@P*t+&sb!Hk*x{Y_zz2H;ntw!gS
zX6_GAFjs$c_W7+-O(rD=IvtLlFtxtY5IS|v;;;8^ewJP1|H?qK)y-3^%=22wW0BLF
zQ>AKuoHaLNO4jANDX4l<_e9`Nk=7dSqbiMg^TnR76TEB4v^je6S&<*Vez8qiux^o&
z%D1kNz)#ji*A8ZDM?UrZ^-cAqVQpr(OwGC<Gc~M4o4!t6`uM}qYfM6K&n<n`%CFXX
zR^eP&*OFh8TS^TtPvg1r?CRB;ti?)-ZLO}6X*I9TC~S&~h<K3w?EKPYEruDrc0w%5
zJEuHp=N7cs!Tz(Jw|x84!|hdj7ad;F^0GNQ`pUO@-s!*P+rK8QUoK=YEA{fV1D^hM
ziI=}Bsjc7ZsU<pl@(0Dmj8m5`6<D3k65}iAKZ*0)B+pBsp>m$h{vszuujmDPwFFtE
zx0Uk8ZG9#=`<8~hxAfAb@~ugWlQ!&}HsOfKBrE=c!@tA5xmGQ$E!cAY8B@uYNe0bn
z&t*~)jRU7{2~}$r{8xYDg`H=&it)O2W&88_PP)mf&%Vid{IL4r35Wd?{!f%!kz0G_
z*CFnbT?Sd*UO&Dc|DMnN?WMo$D~=CGr*1iXYqeM3v6?_td9UtsOLI9mduQxbjQ_Ux
z%{iI50x#AXgdMiMv+Ia?0jt$v(HGh~4{f`drJivA)W^S)w|=c(`S!st@ud-Nrw={k
z3hq#u8{pkKt?4S4(c6CBrYD`B9{!vDa^Z>YuywqDOeB?e`>bF3ys2TChw!4Jl9W}h
z;g05vOZq;{d7WBu`NpraDSvwn*u_ttnxYtJbZgp?6)Q8`S&P>G{FGG~*Z=BIbD7Pz
zWu*p-cSmuQ$}?SBz2LNf#q2x3Of{doJdp6v7VkZumOo8ip6lyH!*HQSZEfM04W~4x
z2Yp#v>M--XrBlbgzIo+3dIbgROl6(^PI$ew-`9F&)c+aQcg-ZueGPI{yq~e^%fUlF
zZc@gErd*yaQ)0D>WBC*OHgQZa@qXmPb%OI~c3S4lq;n0s(zmm=rmyztTNv(sR&+Ms
z!6j}EK><!pr_?eXV|p%q?w+nGaw}A1&*!rb6W$fP=`vC%-5v5}-7J|s;f<cv4__{s
z@=i9-F8_JKmKO!jW*l}rc{MOe({hvH)s-(|uPE7E)ru3>i(k+3$YRIV9mn=u$xm<n
zd$0WI_9AuPS2?G?PVivkl9{iSv2toM%gRYA43j1=FxA_oq*}CEjVts>C}a8VzW(}!
z+mFk5Hj0~z-+Pvz@JnT5xTmG^xtBZH=64Ifc5lpC)U@HJ$<eKgen&Cv(pLSSZ{Shi
zkiD(%e`dAP9@i|p$_&*7!ktQ?;Y*CBu(2=k_PEL78K!Ha6gefwU`imjsp7gN=MEZK
zpP%^Zbz0&++w6aP`Yn=g#rbaT-FNhFtL%A!gpE?mf{k1IGKwoy?xoE#{uZP4%m3W%
zcN(E*XSYVZbY-8jpgyBL*gcc~<Gs84{@&Nm|E+CaIBVVO)z7|NDEJ_gwY{#cHsjH6
z|F=`zC$Y=P&Eb3UU*VknrGFcy@v*P`IYXHBV9lQ`CK<Wgqdvt~X#K0W^tHA<i?iP5
z`15H}7bkx%v({U*fBg(cj%`03>pz(s(ED+(U%>TNpzn?otG3=3jp21IvJhYF%b2-s
zlR4kzNOt>vZwYqwGuKzk>E_&Tusu<oy!Ff?<HI**K0Gk<ZS%9;p7W2b(=7?RT^y6H
zv{BXQ(rvYu*?Z0SHh3)ESR`dJ<3ZrV`+-4^A5Z!?+1T*eg-^Xb%a$*8JMQ#)TF%OY
z@=-;T#HU?86zJV#m3S&7i1(JaY0^>_UsJExxHV=WJ>p)^+;?8HTw=iWG(R=+c9XB{
ztZTi#ujeO3StLezYp~WmYYDTOcSOY5<fcMIm{~;itD5>Nht5xa9Vz)^v(Y!NX8RlW
zw*Gqdut|Q+g>y%bFZlMOAl*EkHR^@1rfkyf7x_n)|KfZxOZbIYYVU={ZZm1VjLpVV
zRBhWMg1I8&_wCnq=CbnRSofUSzPHSFX>(}#W?zNhJPWf~jb})fR58igGFsV9{j4y_
z@TT~eOK~3O)oddsmR(x7o=<!3B7TeIDUn+8{^zp$qs;1^EA6IeWQMY-dT!8S^$AqJ
zcF9pKb`4`u|DyGq3u5zJ{lr4gi{1>oe{ju#X3ti3e~ph1LVB0qTrQyCJ?pGt;JF2>
z%??<m&X)AIJ6~_O_>|yfU76~-mvzhQ*$h^d{u9WkGvAi8eE&5Oy%!ux&t7pSxK3SS
zu}SW5i?07Ee*Zv+e$fl;To)XFubIa<W0~aPvj?7Z>b?;^@J0QAO6rZp{p+l{0~EGi
z58q<yC3V?h&!;6{qdzPU`C0XuXTk5hnwia?BoAJ13JX7c)9t-LbKd&P9@oFOKRo@s
z>B;xU?#CxgK6i5ArAv`sf!+HumIXL8bEkiPeE78Q{W)^WpV@8y``&Tm+~3!gCw}79
zn8UbK&EcSM!zJ|wqo89GxL0cM?h<%?K!dgCq~5P@X4fmPY_~rAz<qw=i*WbI^_(Z;
zg=YQRdiQwK=f8(EjvP2Sk=Hf(0MiuF&6m4Y?BIF!B=C`CzrWauH&0CByz1vOb}u>V
z-n>Xkql%5o$KjxQgOj>Lp{r#Fmj|b%VP;b2nH3Qdr_z=lUL5gi4SS5Y%F}(OZg08S
z``KRZp87?k$H?<j(7L5d0``_EhO31(eZI8)Z|$C+%TM&%RY%V)o>t5^ZHaFG#)<`D
z@3sGjTR*$wbmLx8l}XDLg)PP$XIY%;m|EVkv}|NET6?VDOWZ(pW=7DWLozp$4C+5V
zKKGm>Q*EW%MvMHZDRCPNlXVVFKCwpN(&Krz{=V$D-OiDH@byKG`t8PI9XGpMc{pY+
z%UXM_Z%J!s%tYazljHe*eU`7cb2t0Swk0esHFWRCqb#XY&8{we5U|7a|I>cQ?F+W)
zPqml2a!v8^8%=wksFaFB#dS7c=iK)W5z1V?w7ch&c)ZB9SE0$V*CzZ+I==AyME~AL
z4SdYEznKVbo_uRXz{+K_W;p+SY~%K)uftCNAI}4gtg}|nUDhNSEM;+OIVD<iF8jXC
z5C4k&Q@y_GS4xNqFP>_*UE^_6v0c>Ff8|V*`U80X?>;^;)lGk%ymVP@7Ejsj&C}j$
z-`yCt=G3Hg>4`DNVm3|H+F#o_!}r1IgNGL9szi&fFl!I6h;+TUGih$;Rk4RktGxxM
zPE-5lrBhq5x1?NWg?WUrz{VWS`eonlnwT^eP1G>foc~K|$-Fw=q92nUt&GUbZ_?lM
vC-c}cyZ=)U)NK{ke=ob|YW20#)!)x1eq3Jm^)kzf|IDW(=7?SOVqgFOfmOK!

literal 3458
zcmb2|=HO^Pv^<)DxjduNxHu!RAhnp`ZA@<d9XGyz@8Tbx50`N$O0zI_2v#u2V`O&x
z^>o4dgL{^-75SYjoON%%eP7w$Nnw}X-O8M_OE(}z_wAkuH6C_PJfg*gcAwbx>PgS@
z6_fipj@@98bbfexbwP1-e%<arFJ0Yb+g5+yF2DP{>7IR+;zd6T{+~Y1XMH24V*2FN
zL#tMAw3?K3K4LDnLtv`U^zi4pB5_j#+?{tCdpq~??3Lp!o*OHbW^F3jcH!sJ!hM%#
zfB03a7khom#gJgfsRC1%1vpes(B3woi&_5Xrro>NynnB^ee?aAU3-7NU%u(~Q`hBI
ze~aoFW#i&w@8(~<_0Cf0m*aLv-Fw}J8;=}Zr6Jbx_vyRO?ecA@DGgD(cqfMjtl4<?
zU4Tgl_okn5Did?mmG;G4=BZ4ydL?>Sj72qK+WpQyn<8iL3vb@S^S^RONYT#wFROO=
z%Rcm|yuZ*k%Sk_Y+PmA^&iQam<5X6>^=GfZ`Y@B2UH3y`7+c>=3Vo}n^*hwst77je
z#ZqrGvE!2>c6`_;#q_~(`3hTAv!mgjd=t6ZSO0yQaJ=u@_XAUH7rcGgvnoKlog=KM
z^{b+kcvF|#?FVNkRP9Tctm(0>`1R=<>r~qh?_TG+;mNGR3l9tvHzXQ~yEAQaJy4;z
z^O-WYr(VW`bMK0Gzd!cUtFowZ)kQ5g#*@}*DGX;_d${+lX)v9UpR)NZtNYdGR^l;h
z8fB6-nS7KMHZvvgO}c;F|Kq=PQzlL?dsQ`E?3?*<In4;$j(<f~d1);tx6IU3yT5J4
z&CG?nDl5DmZFVlHip-hc_3e<1l-sqLk^ApXo?#;wn(S#NuKFWlQtu1ytl&*uQ*&3X
zIubI;b8&!>zx1bI<HrkKOdPK2uT6FeHI8s!#nI|s!q)70W>=B#2Zqo;C7<>7@6>+z
z>g%cp7s{r%&aN^yKYq+p<m8UmUln!O#F`&Jd%7_-;Jac$j$)!>j-$fG&626_RBt}D
zmw8&n8DzidDc@7E-FY%ipa0z3Ci3-9-G2G<`Tu$LKbcp4^~tdZ=JxwMHhj9;{bAjm
zeS81Ay43$@uDiE>|NgE2vo}3Cd{%MoVU4x=5zX5zvs{^18l0Q{zfSL|a*IvdjcHrX
z)OEajup&R`ap}i%cjx8)nZ~u-?wFR~>i|y6>cmNpWK%oM_@`y5?a<k;8u{wk-`tAw
zpAY{Y|NZ5k+5IiAFEbjNZ9USKb1kW_E2wL!ObV+PtD>9d-jj)2o@UN|d9KIo_r{~Y
zDxSxM3ubKIX`q!9s%DTLo}Iw1mD2CI@QJAS-;(o}6;=e^Ik9a0c>zaf&6Q#+KW^Q^
z^Q2{$W$Oy9N~1}YdiA{J<`2Kcc_`hT`eCEa?nVF7)>){`++3=n^<>E#_4lC{j!wy#
zy7p9c<_w;6D{uFEm#>L0<({W`et+<$jJ)Hs^|wxS&6Jur*{x$@wwRsMs(_-tYt`xJ
z%TLa;C<w~y6|#IMwDaY$%sJ_&O}akK&d*_47S(VgbFPZCp!)|+u7lzWGd+2~WmX<E
zHL`V^RF=JICR2R;eTT*+E$YXP$f>9|)VQ6~sz_DkxAnZg?~U!U_4h;-;<f6oSy^!$
z{B`Qm)e6l8TwYtOr>_!cn<?VoY!R&~^kuo|>!fA6wFjO(y;_r{tiNzlt7~Lh&AT%S
zMmjn=A51?#4+>r+F-1v!>y=u?Ox^!G1SU3DPxwE*pgh{HZq0RVtDaL!>~?HxE&hMK
zVCVnm8`R!@Wno+#X_m`7=gO1jS?k0NE1&u{h2-RgYEO1NacNt}RZ+#Y%R1Cgwxpj_
zdAX`deeDHx*{#}3Vy<asPWohHysrAgD%0~fu6SM5i_HtU^f_sxphWIERTab5CFhv$
zy!iKYQqzVl{Jr09#w_Rx6G{tsGv}~Qj@qiM)PpG|L54OtCG(f?PL>Q0-+g|z^QOS#
zC)3KhK7BZA@Z^K^o%*G0S<&*F_kCcRtJiaDk<h=tFAwi_s{PgMEc?;L@*|7t+YR4V
zO<HWYfAu8(rLNB}nYFaIow+wb|5sgQdY>OhNx0YHg8prKA9-UO=Rf57rM>gewuRZt
zbMBw|_*e4Quk|b6KKLcRG(zq4p@$AZ`?6oojndj;6~Q{=>%R;ok9ivM@9+EY$JJ##
zy>-BUvf-xFU!r!I@T7EY(VejP^0KHR(NJNBR~+Ye#<gwlU3=f}+I^1Vf{AO^7^}_g
z*`#Wy89U`NYw_BjpRx+$`d|I&E@Sz=?W@h=-Ci7}@=UY26{Z^&nC&dB2s+n!z%YYV
zPip?zdph>EBCi%N-lD=3&L$kQ;lY8WBDLAF9?y#VBo?h-oUYZ)Ei-4XZ~Ke76JKv#
zUpBXGZT;D~S<*b|?JFlt$TtbKN>5Z1cIa8->7lgbP0-BORSd<GTm!r}tDIw5F*jgO
z(zI!s&w7?rl|=_sY&-R2MRn<wn2j$5ybPFv*ad`GW-nnaG@R!3DAmDf_k!l~eU>uk
zWcy+nn}fD{yS`s_@?bT`nyKRR{1{f1@A$cA?%|iN?Z(Gt_`KKosZX1vEFCQC@_v!f
z!_u{nN*{ju>ZQ=v9Nn3H#`|xX+|Bp3;dQ#@mzJDc7Q^3}vf#i+%a%z|mTptDJed?M
zIinsg(hgGEp0((O*A}e@dDlM*8h`sXLs|2~rDun3%ka3(SNXPzE&Yh4?ez!6g-L%k
zCisR3n9X0dBdjEz+o62vlmEPIFZnyqUi)aD?>~3D$60m$wJc>yfmg1IuH;#I(D9{E
zkeTD8Q11Q}x}Ihdr&hGinh+NBJYnYC=N?~6HyhlaXIg*HeU4%7`eirW?mzl>s4tyk
zLj>>ZVB^-lFV8;Q*n8F_{msshFZ1VYzZ<w})^_f#m-uCi4*ff*;48b-R->l=_q+Q1
zdtbxz9+|{m4?p|%;FAZIyYBw_`E_CEd;9Ida-MP}6&BVL{x@6v_xR16SZl%YEZI+l
z<@3kOmlkZjyWz?HA0dBUE_waCFM+e(>iF|%QWqzGF0<BKw154KK#pxc9qT`t9MJo5
zuU|lQ@8Ven6Blm1FB;41T4W)<*vBz*+a~kAOOfpM{oWGn>6fmrmeb9--(Y*9I(h4v
zMaGYB%=~y@=G*3HyFKS0U#D9Vc6)PD`l7VeTPNN#^NfEzwa~*=t9R<<0|#09x&Hg9
zOUO^}nSZX+uzgy7iixSLsg+pN_7rd4e-|cA-m_tjSYMRT!xqh8Pg4#3s~uB?Os;B_
zR&G4?B56;6k^QNy=M-B5HR`ob-xA9y$cQpGTU+0h`LQK)t(xWsWA#m!KB`<ZbeYV%
zFm=PhTfxtNFBYqt7jyp9f%qvK!=?Tl{I>3@IluUygw`@WJGQOI+pTy1)Vh!~-{Y&|
zw%&hkHLK<|tg~#)W6W;hi`jCsKw<XWi;<U#J4}~Oxcanxx6zUXk6Rv8*?qX25gu$6
zQEGmhWz%_qU10``XF4udyYN!o;rQ|*Ik#M&Z>@W_h+o?5$se|4Zpo9?i&yzyWS<wj
zNoQ)m`tz;sy0iB$w2}9kv_-3Vl1hX}V^B!v)RGCFqS*nv-7j8`+@ZH!Nxgg3^RArL
z?+d~nJX~_<u=<pWidDyg-vo2aP(Ax>M#;GqtBg)qrp})E>gJnHZlCQ1Z+=#PxBhF~
z5V-bpyTj+*8&j?SZe3QOxZE&k-9ClTCY7TTzlx~kR0h@6bTMVEX|M`#kl%9t1J41I
zvl4l1YW_Ki^BI=eGcIF0Jg=tYYUH7&m3#LsTEm#>)BJ3z`r7+V_DfHN&rWB!TmJa8
z%z<>Lc<#th-gN1`%3Q1V`YFfWmv7Ub&pqjWzr1X+pO(7&f+d@$ESgpmxW?JBRd3GO
zetv!P+TyA?vwq+Cwx9iI*}M3Dms92oGT20X8V;#5EcIhZUD9(=ZwV7u=*2ZmlSK^F
zcE7lNJLY-d{dYXg^0jRX<K$BJs;T^+cj3!=HhZx-@5S8|+5G%&2Z*q0tuQvQW{nb`
zesPYCm(BB!Cz+<sopa3l<$LagiCcbT1T1J=l(ygji%1od#xE9)bq$9(RydyM+<Hl8
zqGV(1!W=eHxuZepwhy9|G{3Jk%(Bm_F!8v*cFFaF4W5&x7wM|DzM9Itb5onpoay`C
zzJGky-nH(_&D*c$Y@SoRA?nsAiEj71uWCQkZ%sa@+wxX-xx4cU>6S9Kg)<#a_%~db
z+hA~Qf$!>%$}5_dsR;Xe?J{uRCUPeJ&yLTQPP4X#Ob(f|U16qp?irEp4=RStiB)%k
zciaEn_*^VewZc~F;rp^<O@`GQCpaoz4p|#|Dl;=tDg4orzbEC{|NiW^pRYW-s@bct
zo#(1_yblBSsgUVS$`7yonQqT^x9L{hj(-^e(d|B)m;bTIocNLR{LhzHitF?PS8grx
z+I50s-w&pc)$PZ2tugp}w9k3I@_eZW4t-3wznM(jH2Kzw7eT(JhV8$OSN8mn6|9Z>
zBYENF3X#=wCZ}~AoFZf*7`E<3aoq2x2kQ^DuMN4d|4E{PnwoZP9^>PtV!NmnCmzYL
zakTw!J~1)XO@E%ebXjc{PwDN=)81;|-59niVQady=Wd^!DcYfRzXc6vADG_U>VDf}
zn^r_F-@<}T3l<k2wGv*fd&o6xs*;wj@0+O+zaCY+d>0Xrzas6*tW@ux##`?%o5*P;
z-f1-X)5`gdt6rX0XqVTV*ERK<+K)r0=cnbo`W(;sCfxetr+WvZ_onaNQ+{7&THMyv
S;ld04@vpcxG1$_ZfdK$-g~4e6

-- 
GitLab