From 9ea8a6a49cb443872b1255d9007be698c33ece99 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Mon, 26 Jun 2017 00:01:12 +0200
Subject: [PATCH] examples: add the missing proofs for type witnesses

Not done: double_wp/logic and avl/table.

The subgoal pairing changed in verifythis_2017_tree_buffer
in an unrelated VC (see the diff for why3session.xml). FIXME?
---
 bench/valid/type_invariant.mlw                |   4 ++--
 examples/avl/avl.mlw                          |   2 ++
 examples/avl/avl/why3session.xml              |   5 ++++-
 examples/avl/avl/why3shapes.gz                | Bin 6961 -> 6988 bytes
 examples/avl/tables.mlw                       |   1 +
 examples/resizable_array.mlw                  |   1 +
 examples/resizable_array/why3session.xml      |   5 ++++-
 examples/resizable_array/why3shapes.gz        | Bin 2433 -> 2498 bytes
 examples/snapshotable_trees/why3session.xml   |   5 ++++-
 examples/snapshotable_trees/why3shapes.gz     | Bin 906 -> 936 bytes
 examples/tower_of_hanoi/why3session.xml       |  10 ++++++++--
 examples/tower_of_hanoi/why3shapes.gz         | Bin 2554 -> 2606 bytes
 examples/vacid_0_sparse_array.mlw             |   6 ++++++
 examples/vacid_0_sparse_array/why3session.xml |   5 ++++-
 examples/vacid_0_sparse_array/why3shapes.gz   | Bin 1501 -> 1578 bytes
 examples/verifythis_2015_dancing_links.mlw    |   1 +
 .../why3session.xml                           |   5 ++++-
 .../why3shapes.gz                             | Bin 721 -> 794 bytes
 examples/verifythis_2017_tree_buffer.mlw      |   4 ++++
 .../why3session.xml                           |  10 ++++++++--
 .../verifythis_2017_tree_buffer/why3shapes.gz | Bin 1693 -> 1776 bytes
 examples/verifythis_fm2012_LRS.mlw            |   1 +
 .../verifythis_fm2012_LRS/why3session.xml     |  15 +++++++++------
 examples/verifythis_fm2012_LRS/why3shapes.gz  | Bin 4858 -> 4936 bytes
 examples/vstte10_aqueue.mlw                   |  17 +++++++----------
 examples/vstte10_aqueue/why3session.xml       |   5 ++++-
 examples/vstte10_aqueue/why3shapes.gz         | Bin 447 -> 480 bytes
 examples/vstte12_ring_buffer.mlw              |   2 ++
 examples/vstte12_ring_buffer/why3session.xml  |  10 ++++++++--
 examples/vstte12_ring_buffer/why3shapes.gz    | Bin 2258 -> 2369 bytes
 30 files changed, 84 insertions(+), 30 deletions(-)

diff --git a/bench/valid/type_invariant.mlw b/bench/valid/type_invariant.mlw
index 7664e1ee21..87c552f85e 100644
--- a/bench/valid/type_invariant.mlw
+++ b/bench/valid/type_invariant.mlw
@@ -1,10 +1,10 @@
 module A
   use import int.Int
-  type t = private { a: int } invariant { a >= 0 }
+  type t = private { a: int } invariant { a >= 0 } by { a = 0 }
 end
 
 module B
   use import int.Int
-  type t = { a: int; b: int } invariant { a >= b >= 0 }
+  type t = { a: int; b: int } invariant { a >= b >= 0 } by { a = 0; b = 0 }
   clone A with type t = t
 end
diff --git a/examples/avl/avl.mlw b/examples/avl/avl.mlw
index edb59d3521..60a7611fbd 100644
--- a/examples/avl/avl.mlw
+++ b/examples/avl/avl.mlw
@@ -172,6 +172,8 @@ module AVL
     ghost m : m 'a;
   } invariant {
     balanced repr /\ m = seq_model repr /\ m.hgt = real_height repr
+  } by {
+    repr = Empty; m = { seq = empty; hgt = 0 }
   }
   meta coercion function m
 
diff --git a/examples/avl/avl/why3session.xml b/examples/avl/avl/why3session.xml
index b55940d100..93e19270e8 100644
--- a/examples/avl/avl/why3session.xml
+++ b/examples/avl/avl/why3session.xml
@@ -18,7 +18,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
  </goal>
 </theory>
-<theory name="AVL" sum="66e1443365a42b282492937f4d09bbb6">
+<theory name="AVL" sum="c0b96d14d5a90bf2332d8dc606653492">
  <goal name="M.M.assoc" expl="">
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
@@ -50,6 +50,9 @@
   </goal>
  </transf>
  </goal>
+ <goal name="VC t" expl="VC for t">
+ <proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
  <goal name="VC height" expl="VC for height">
  <proof prover="0"><result status="valid" time="0.02" steps="30"/></proof>
  </goal>
diff --git a/examples/avl/avl/why3shapes.gz b/examples/avl/avl/why3shapes.gz
index cda32365530832dcdb3c8661cb89da7bbbd8e1b9..4b74bde90c9487cd117277d8d768bf6b4d8be19a 100644
GIT binary patch
delta 6345
zcmdmJcE)T&98<mQ)CC5Ud5&h8C0Gd>GU_~$nR+NL`Q0w{%@=%F3IgJ?X5L-xxp!;0
z?<wn#S^C_)Me7{QL~=^pUMrNc9o_Qv=9Gk#{Bz$9e^0Kz=lJ9A+1QHXLf;oH=h(6>
zNiFrNT4>_0LrGs-?|=QvZl)IA+y7$8HMX_tg2p0;*&;-iZvJNTvOX^Tect;YOWW03
z%=1^&_x`>A{|rmWL)q5;`F0olVy{}x|DLw1db9rShi4hKgbOit_D=0N<z94Yk;7r8
z<$K=U>p9jeyMi(ENW<Uk1M>v;uGsSb%e(jf_ul@my|b{E^}+OtI>mQVkGq{xH4?Yj
zC~7)Q2ve+z?2VJSegCG<pNGG;*Rx!gUCm#A`taK2pX=xQ-|c_;_khT}KmVr71Rr^?
zS+vIT^qiR!Prbk6u&S!wNyq%oEt&0!{HM9rPc>&0sg^67^yWxu5$o28`<7pD|CXNr
z^4+&IH??ocpCeyiFqeDtaq~B~xhkhQ&OBQfnZZ8o@RcHadCrdq@=TMqS6%J;IPdwH
z-ul1yH(l?z=w0(}=J)6ycV4+Pt-fd-_kZ!fALswCYO<MRR(2{f#NM+fal*k#u5X#E
zBcD#%zH~*O&vp5D|ErH2-p%Cu5c2QaLt)$bvHbd<rb*cSx%bsCICP!w^HnnI4&ClI
z*`$AJq2Vk+_Kl3X^Uki^G*PjA`4O*HTe&|qzVUHu_Se7rEV=%t?V-;ni=$^se`&GJ
zT5jh5`u$OcWXZZ)GuPK=?XKms&6C<%@xSqw+T+`g^VahzCx1^?(JQ+f#&p`QWYa~9
zc0<K9Gj0~g0428IH%X>5C+M!yT(P+ELFts~)90MxioMm&bL-QVS%**V&AayPs-Rv;
zZ_4-N#6@of4`0qmtY<mwU)E`MyWv!l;3UVzrL9v={Af|1mY4sjv{zfKIH6DbU;Op`
z?#6%i9Iou%IO$PGR1ep&?Iq^3Pwropmlf_kFDK&t{bM~6!aLt@KW4bi?{nhp4Bgva
z?ipQTe#H+`cwDC1Mx9}MGTGle=i;UJiu;zTzt3Nv|L)Z3iBsN%zIuASUPJM~jQ<BB
zyuJ%vh+CVfwC2pu3*Q-q?v%Yz;c@w%UEt)q@P+d6<*F><EopmLJy$-eSkz}&W~u0L
z_k^wV`~Q==4c#stdR}(Vrgvk6qk3+hQtpCZ6W6KD$zkRQ+qt*wT|?^^xtv@k<v4N4
z;$n;GEvnn>Em=>5$hbEin&YZ?eedKwtSX!~+6sY(Lk}+unEaB}xjv=g(({!wcQ?%1
zxpUUr$O~GWGh`$34yD}m+!!+XccIHGPWLl@w;GkdW*PY~PZMZmRqN}Pd0T1Z%JIBc
z=$?D&sikL2j>I^eKNE9aWzCD3w=WrQUz%=nCg}W~u6e$Zmj#MMc-m@h#MXuiED&9}
zX3=_2{iWv?33!*;&t#vRVRE9W-mS=Uv0(Tz6RA9%43+67s{~#-=oW81JNsDIguSIa
zn}w^qJ45|<tMp#l_+-lA!0IR4&P<G%Ub{1^=a@@^w`IhO<-b=S)yQ3LdVRh8GvjZv
z)!bK_FERczf5N?Vj^!^6Cqa=#4_wvS&#6s5Qpt7Qa&kMvo1X%~-<#I<&#b6;v%I)|
zD;LL~t1bO&AMxbPpL_MvlDSW^l;?VBy1&dm7vAN>=KW*?i)#Vr9NY6Hv;SS)f2fSV
zSx2BDGVAVvSt~DfwrYHdD%H9EaDCsW<(!`0m*zd3xT*2+wnN))FZyut=Y%~0#{(N~
z23hYvr?CH3;gN{9OYV4@R?Ml|DzWtK7B<FP`}iB{8MY>`FRPuw{^pGoOG3b0%}s(z
zvaOnytIs%g_VH+3o~dvk-f7aGph;13Z)(prFy2_BSNbeY=OCx|8^2wRs$a9Xm?D;L
z5%_cOX4It_F(+5lBxvgi1TUz*sj?wHf69S*j~^WKnYpmx;W<k^zEwM4)g8V%$&xqi
z=|#m?vt;!3SijX5A5(auGRbM?IcCPJ8D|bV9xyo3<dy}BlWT7UZ?LvrF>Gcj<7BG3
zXL58y=J`Wuy_OMdcT!9>5>8!>ns4WSQ%~SJU*g;N-<8){?mnL@``ci*)wR(3FZF->
z9bQ|Qe%b!>gl#i-9ACS~*V**=oV|j58^Qv!d9So+n0%UVWz?BhZ-4J>W{F=_mwI)r
zZF2A3X&sw`zaO9fbCJxM^QHe^f3fzk6~DRs@Lac7ivp`8r-&z<&`w?By1c1O()-kF
zkzX4>Ptbqw{N>p7tdLGA)79ZxY7r+4cggH2&gr|R`K9*W*WVne&1$Y!-h6UBr{m1o
zQkc?M<dw6-F)twF-1GS}oDS75Ra&z}=Gde#R^!tFK_?SAS~bQ08R%9YF?nXt^4Iow
zHsh8Q<0m<seMdV}dJcA8&@Vap=ITAegD*;d7E}j^w|@z}V%W>~_;DNK%lG~oiDk}g
z$3wKvY8JW`Za&vp`Ez5K%586%sTT`WY^?bb($nU=@89%n>%kS3j~#wRDSmqMpnh#p
zkoIa3qZ4W&w;b*)xZtK|@#pKeHnHuu%)@JazuM>B5Bza^`S*O!cV%a8C8`zOumAS1
z=u-0Gb>%xn_ov?Z%_jWpjdzA@^|P?8|1uWo1&O{6)sxbSonbKVaos}831<U!HAS3%
z{pJ+Br0(KTFD&@0qIkBI*%=p(V?sv!p08@_O$8TDbZE>~Va{4@vN)U3${-@;m4)k)
zoY-$_1#?}#Pg;0!_3C_G=XX<hc2=Lduv@L;&DPR+bN7}+vVWTQP$|LTebAOoi!U7d
zW3&2o;;yKFGq@IseRKaD=6&@3i<4{CJElu-efO$KvNAM$g|AilyOU>B*Qk1==N(V3
zNxizhut&6hGv`djfR4x=Z**oZ;#x6h&N9tbw;EaB!iXe;_Dz?|gac<yVp=!v``q_x
z=KJ#MCd+uw4wYtc>zlfIdG6aSBA3{>L}&B5pE$u7#TYD}s-?QrL_(s1KlI;9-dSGG
z*%N<HsNChotmd@UfVDfZYPyN+vkA@rgHD$F9Lf<tvCc!nr~X((SlBg-3kI58Ope=>
zn0KmZG8|E8(TTK9JT79T=3ZN25q*$J{Ydt+w`zO8Ryb*ID%<ffH+8LJ=SIEdYJI7>
zvqcWRU|xJuYLVa<5v}=lePYMU!ZsLlX6^Y?8sTGbXTF5zUg=3ct0JB-&DOU3m2x7#
znLlFU`ExI1r$!zKjD1zVN0rHUnxglqgoPQ2T^v@kWW2c=3|lJVw4MlM9^bm=@yyC!
zp{$wH&DM4F&h6-x|8&Uzd-&%-scq*xT)l!W?iBL;m9lAS-{Gw+K~H`!mHj>C`BJgX
zC6CvAtc?)e@bp!?Sa5v4+sYk(uU;$)Tx&RM7l*CI+NIi)I!w=7z3mB)%ddapw6B#b
zL~Px}Ma$O8hiI*qy&e!!dqFJp_1<vq-xov@_k3wl$SGQ?GM#0&DcfYp+OD`YK`(F5
zUQ*dn<yp5ywO_Pu%hhJy$tpd;U5l<-Rn3nnndfYJ>~@p0MJh|qgqO>ej|3jfS+P!h
zYo}4#BM)8Hw!3z>9%xJv;JWKPqb^CSKGij<^?=2sh?`21^BH?L3rso_`E~VD?OBl*
zRxG~o!2jBnyn9(MA1*g2d9u%nZ_O9UwI||k?C5^B%_8ly)dug&X5wr&87wDvD=yb*
z-MrAhcgx2koI;(OJ+?44Efc(7>$!!4Q{P8vsY6<uvlheeEpygRP01>G6zZ1v`@sMG
z`Rl{$Cv7P+zO-$3o$L)0;ilS~&tBHeKUb!<#QBc<<u3hg64%2m`i$1)Z>`DEzJ1}y
zBO7mTodXvxitBgrMs-Jgw@KAneqHAFUoGE%hLI&aJ2H%;zZ$NJ56!vJ-SD348go&K
z$e#vRxyQ%vmdh@jqpO@V=Zw}O{e?fKh`K!7V<uO0$+Es9<@Dt94-c2_*tyzr3BSm%
z15YyfrI&MZTmJs;I<HnGzuWAxsq}177Xxm&nA&7DlTz#M@LQ)k7HE2&*wn!MT!H2I
z#Z!?Bb_?HT{2b3#!v8pL=PKUX{P(=4?Uqfr&HLzUN&VJ<-xs}huxUz9UuxPG8);Iy
zpIh1MN>`%!aqV>P`XG77oUW6#E-y3Hy(S+O%)L>%sI9h8GAGF?UunTPz07YpCs~9~
zJY&&Z67Znzb=Jc}w*}mo*LwzTRf`TXiTAXbwkXwMcg!RETWYE|f`napt<;p~hDfw<
z`4#-hw^;D`exd3S<%ueM?nctNks2$4yr!H=n`;!M?0hZdLq^W;x%GdG^5d4@sQz4d
z{NwDn6X)x^7p;FOnD9t~c?M6!)6G13EX|Iq_Q-9hO>Qvh589`#JZn<dhn*{OHWfu`
z_nayydEIo;?m+<?v$@~HJhNj@nbvrUcBEEsW;pVF+RtubSA}|&<2#+Iuj@+4EL5J{
z7?7=$Zs?WX^u=jahRy6{LhW<v&6H1lc=`73>;Cum<L=)z&Dq~`&F^=P;gzK^_nO^O
zBcgSykN-<(c|E)T%fr0MS1ZI;7oL1|I8eH_vmw8B$@VGlUY&b3ci!aWO_P_++jTK)
z^X<td$7a70bN#XKzs4uYM%~!**V|Mi!zFId*J%)mEp0MuxMF7DHQi{_%J0)ygVyNR
zoBZt4x5-+nxA8?C)17DyD~`gwRrf^rp1Bm2>L+Y6tm@=&WB9mK-)i0SV82gwd2Mwi
zL1q(M7>}|D%DiUuh&B%`UZcLrU`CVm#ImXxtM>kBJaN}z{$%k|?dd|BHh31_n#wX^
zYchjkn&{NOx34qT%_xvx|2TS<+~I?2VyiQ4chpaQ*FMu=YwyOA(w3{qb*VkpH)n1Q
z;)v)i{3^sI|7+dz3fW3|%e2JZxgyRj+s?esaoqOPQ*3*i_59o%{`{>wt*sbR%4fCR
z%(y3Z_}8;vS$nQ0?seB)&1-um^!@GYv$rp8+qZLflH9&M=JTcdUDKIe(-z9A`KxHA
zJk6H1v6#HA{_$>J4<jv${_o!%D?+~}?f+bQVQJif?1TvMsaLLZ|Mz;k_?O$`$MavU
zQ<5=z#j`7_T)K1Oym!S6=dXJN<#+z&?v*#Tnw90hBI;R=%<QZ%)ApSnK1zX`ZZ7CP
zbV7*d<m9enNyQ4^&pY%VP4;o-J87`*%+U?z$rl+f=>+U_(70DWXLsZ7$xG^_FSas0
zsJnA=+A&SeP}76erE>X(w<J8}OVyn>f3!1Cac&7zSShuG!J=(KNO)1Ot=1b2y;<)%
zv+jCt6=nZ#bgSzx$LUE4%XaLmop|ru?Yj1&$tFcJoXl1&IFbGB@1)MdW}Uo3H!}Pm
zC>;p(x4pOgU$gLLPbS4m?)osPz)gI5w><PttyrmI6WRG%vPeu#YS!9}KaZD|F7_^(
zxwv0wj{}dQ=-e9<H-7Hoa5@_N?#!IG=l<2&cgmlwGk24EDxt7UB1O>k$E2BVhD#!*
zgnv$E=-X-h+4w^8+4-#r%^U}<^%buKe`QLUx;WG&=dkad_|OIHyTsRVz38;Bmp+>t
zF~iEwDsQ)O@jPqkaMmm}zk-bXNf*B|97$lzaf%Guq;%n9%2WRAruR?J-{{XQ%V>?Y
zyZv%kmge*qih``Ne#d_H-#8X`YW~eRURrV2{?-Ww-F@74>PO0n)00|%Jw1P8z9rv5
zp=(RM#O4-%&CyNS>m0C1j=l2Uu9J+B_B-keHnA;wI$^FvzFTDDrM1l~-2O}dY;#N3
z={RaElO#UvfYXFq!A1usn-=Xgxv)7@_of#6HoY>j!>7(Ys{CNY-!I<YeZXs5)c2`P
zoG<m<p1Ub8WOiY;%Zywg(L8POqy<K)>3=mBt6Ud#)f0K@zBD7)pxW$uX?b)|U(g4Q
z#iapG^+FRTUY_aZIX8XE6~V<{JTmW!^lNdwTyj~kCU$LzxE8Yps~WqtmE5npZ_{tB
zX(~DXL@xgAwe3-1j=O9b4HouCdAOS2zW;4YAp0Sn*VV7&dd@ESwz4bjf79eS4wHRX
zyjETiAvS-?Bz`TIDMzx{x6Syfx<kC`>B6aZP946VuKGKrUU9elwS1dgeKF@V)51#o
z*1xqV%UL+j`O#E?Ni7>SH(cc7>2^7DZD!7C&fqNv|F#zW*|8)?rTqurT(>PZr9>hu
z(o~rlYjju4jbz%ne4Z}v#m7ran&%m~ipdA^oXlC=<KVU6M9(%?ySX#xE;(jf&3!%f
zSm<|V_55pL4k6*pKTp-`DkVGDocQ;BB8%TSW$6;`D^d@Rojv?a>g_9ciA9Ee6EYW>
zG{12<6rJ5Il={_V_FAT+KN{{-nfS!-jmp3GZtAPqt5<(Kc=@&Mt>$CD<ZjqH<eKDj
z+t(IXhfaLRyyMJ89Z}Y}>iI?2+G_Wz_38waW+o_EOf`vGb5bsUm-N9t=Xx)u1a0?6
z-wj&se_-KRr}QGsp?Ov4GDYW0?~<d=Pw=R_agoJS^@_%lOc{%(H|2INTGM%LnUF;m
zw?{&)?Tc?E_f|9~y;4^^snM`z(cL9MO?`H0eK&%potzlz<mjj_>}m1dV7HubTm}1e
zgLfUjs@$9{bL{V)lm2>X-$wh4i#Z|nY=&AH4_-`tJ7MC|1Wwl_NxH!t5<D{PuC}gx
zddsT+W@@cjml4~&XZz|S>YHR9Cw)n|E^VJty#Mx(J6kt@-}7+wvDG=RKP6w7bzgO5
zh>zIB+L#Fw4_?xYV5zzqeK_gpp?>c(YE~0YR$P#4UfKGJ$?q9Q-=3*jb8g);bGNCG
zGl;4W{_XDdrmcu$;k;+>opmCwzTdpz<5@#b)>DmEPtSkIsW0>R^}plVZcjh4)g~H=
zUMCN!uDV}iDCTG+SMaW;z0IE6cbVK;!CSXh%rR0sDREOl^n+`b(2;G{o`ut#rT-jA
zmAz%~?#M#j*9xm_m!#jG|FH5O&-8yfCXELg99PYrpj*Fz|Fmjl=>Co=YlB|?s5&lx
zoo)W!&S+DsYm;la9lu3pJm@%F9c&`_UvTfgrx!MOW&{ecwH#W&vG&A4iT4U#DrUD{
zrz`whDHGK(vvsM;)1?6t7mY5cE#!Uq=;D;mT$`9T)D?)P@H!v1nZAbaTW#Z#==TLn
zxIRtoTR1N<+_Yz*U_HCEg3XmFv)UKwPFy#Cjb&EPlQ~Okxg@78D=y*t=GIkxCn-yB
zn!KXrr;YQbZh!s#sou%zCUIWvg`7@R&U}&AB?KZHk`C_Hk*z8|C2??9-2o^2x{xHZ
z7f#hSv#$kCm_9QrYumdGsn?H9tFB#mYn!fB;Qtr1*WOs<?)6%2iA1emy_(3>*p&VG
zOT-Nmu5i8D?zj8bacL>p*Wce+rL(21@~xZ~dwNHFXVOQL8}@lsOm_;_U*)j~*>~)?
zMBjvGR{Y00ywBzczmZA|lopd`yW}I<xvTD^ySl)eGd&!(tvgP)Pw)$TSu}OAaOW%g
z9^G9BpO~IJVK&ptcA09xrj=@LTf*wCT7OJE+V38H*<!!V64BlIy1_<P*Urmy9(cId
z<y!9S+AGl_zxD~0{C{-vu;tg)KQ7LG9e=bRg5JmcVF(F(@y6NlA@^i$t!*9`JzTjA
z=TFyub$wRct{)fst5f(-EcvnV%dJlwGbXVcq*@s)owjfJ#9eiEmSWj+93_jV9IN*f
zIavHa@$j>UrQM-j8@76V+_?6`n)g-Dif)?4WC~SGG}v6^d4iRT^HKJPH;+uZOt=%K
z>l{+nImF!kMo{dm?ElWzi?y3s9bRlVC{^UtyWVlHedF6kJ?7+k)gSe$KlCR(_%7Hi
zAg6QKU9jiW*8pGFV^vRnd^>aXXqLeyanoCe>vyP|S(R}9JAM1jg&z}MwM7V9TuL`J
zKD1MW_jrz5bkT;b7a#g3ZE@V66*OtqoCbxpi`T3Pn-U|Ur{*>}<dgp5T7z5rC*63i
zvN8401-TPymO`94Gh4hS1sN_AxOi-N*1L&jHB&OLS3lWM-fNh!C+y9i(7)>{Ciyjg
z_T=dE7l~e0|9GXKT)q9BOkXSW%Icg&(ULdwPj7T96cCcIm^Npo*UlRmuV?-{crszp
z_rIRAbm#gn%iR6tm{Q=4yEm3M{@cLv=&;YT6Bo7$XRZ;7YyHK@8|-h_rzT)|NoJj*
z`;KQJ4xiLdI7LYc6#d;Z(R8QWs=2XC4s<=AyDcr*{KWOHi}Ew;UH?RRnI}lHv4*I!
zOm)%hVR*%PVgfT~e9gb9tu@yS3VT9)WTNf;qYceG-~0M?1{u7*-T6N!(nER6CpH7C
zhh3MK<Rpqn&Y5&9I`l=j*rqhay`7!CCItqsmE5x(Zf?4}?S<p>h`Ln8ttnX&sw*|L
zBj;>N;PzYk?!cz6!Ya!z)Gv-au9O{b{gaLT1K;uoj}KX{skzYqd{5W;vlEY`2@AQ)
zt6tqKw?#+k`LDI1Qx<R;q#3;n*^$<l(C@5q_TnSPYMpZ`PcmgDJh=7ktZhV$?c|4Y
zHI~0UqIcIW$rTP<qQNT0_sf-oDTYf(GC}zD9L-1JZEK}eR2PME1{kIJTr8~r5Z`a6
zu++G5!so{~{`W|lh2&JMaf`H>P<%;Z<z8O5h`B}E)Wc<J<C{&a=6#iEUQ*?3Y&mzX
z`o_6i9yi2KXL6g$b1r47uTrLoW6KMk<I4AMC_LQexT*i7g6Qkoz9?gc04WEi0H*m|
z9{LM9CO_|-6XW-_W0C{^rSr$w1qChs=xazAY5mJwnIbslROi`?zv^zj-E*SAEPeX!
c8TVhxTyvfzb-($}+5gO1;t!g*=P)n;0O4mXtN;K2

delta 6312
zcmX?Ow$W@u98>+&V%ALy6BZjsv9C1Nn78`;G8X0P&zqiSuU|30T%fMLSp42bmOU@-
z3q;+WTe$aD$EiE|XP)WnsJyq|P!w-!w`g*d^p<%pX99SnT>__^yY<>-FW=p}_cqq?
z`*Y;q3-~Yfd;kBL>Prq;bIIG+E||NEYt5?XduP78_vUn7g)zh1sV?;nNskp5f0{UF
zi^hcw3>xcqn=k&Dz@FtG6}kCuwnK*Ww>8=SU*5exf6wjzzjrwQ<~pE%@xSou7cO_(
zxBXuJ-EHN)ThdOatUqSiUp^)gFQVnlx%erkr(n|-u8XI$S`OWiJD2u||N4H_9q%G)
ze?-gW+0Om{yXIA$PCfgw4^O`De=?(9sm_05^4Z8|XL>^Fp0fpA{Vkld^Wn8;J9w*Y
z!W`D_;aqS-c*EtS<*O!Zuju_^+iJI|zS6sVyScH^#`u}%quTd<Opu?y)%=x8q+5a+
z|5+#N4KmB7efjCp!CtmnaQD^KVLjh%((~T@pSIVnC+<=4`91d!Jr7eCis`-g@t6G9
z<Ms9b!bP7<+_G`<nMJ>JlYAO^;&ig)Z@ku=zDL)!G-cPnA62Ww*o)4WG%WwLoqzs|
zpKq!vCT>6S?$7si<+D~5<ywV5EfBp|w`5{%AYbpr9)^w+V)9*~W=1R@rbMjVa6Enf
z`j@A>zh1Akdu+Pjy~3_CPrJBz-iG$qSDt15-7ArxbGY8$`tw)+-0kNV9yeSp_TE0=
zc1lh4owrvLQ{L3|967q~wpYT<c0V(z=LTv=&ZIReaCjYg&=xySO?Z>5DQl#Oz@ENO
zpC$!IF7*CA!7+MXSh2;<>t}E6vpUqeZsMCd9iJ_>NflDMJqZ>k^e(1J2Sn;P8Fg%4
zH$g~p{)Z!%-umuaS8q{o$o_1{qyMFUt4$7{x1O_ILR+(M#nHH`8t?MWGykl9wXAIG
zlap;<|K*<PFr4_iE?Xw~wTb+;&TE_2mb5I(cxb|Ibj%^-=HjC{4t76F4vXpjm3tIj
z_37WYU(eR<k@0*Pw=}M<SBR<SCx1_Fi9X}otFzP&otnd6E3a@c_qgAoIERw`Z0c7;
zy6lSfL^u_=W*m#2Fh#3R{guS$X~Iocdhcxh_)mYQL~_eL`|Y2fW%eB9vdSzL&SbvY
zUt;<&h5JS1({HzSGK*cR-msO^N=00fxwv9#i|RIeOV$%1GVZC9FS2TJp3zbWJnVjW
zq32{4Hs|^WF)u$~ITPz}_D;;%Z#o%MS<dk3m?v&}vm|2G$-fp#Ut5&Z)ZZSMSY;}?
zjM2N}5R>q6*S>EyGnHCCyK%l>Z1wa~npKkCg7ma?=|W*&&g8zFdHa&FT-wU?JlFHf
z)?{*6a<Lt@lk2{w#c`o4B<$jKl_^2#fgP&5=bvfzG?7YitXJN-<YI?*uoSPkn8_q>
zsZfs61=Dukdghz#dg7i{+fB~BOOLEt9y`hHWkk`bhbwH0qMv!JJH0Q))Gb+Q!%`WY
zFPHybO`5Xp@~qd_`9Dkk?%T`y%JC(`f9X%HLFZ&@MHX^!1%6PP?3_N?^N~&K>p3T#
z8NStYtgJqG?YNJP&9}=t>!Vm%{$(9H9#+V<{rtJC%u9YnTPON0owE3gDZ93-VzX*d
zM3d4EmUHvcclrK*6`#1f-BFC=fX>#ugtH+pk2r}`t+kr=`a`(;&&w@KR5Q<i@VI%P
zFgo#eZs3m>H6C#*9%~%PSvfa8eM0<Ki=;JWLGPAG+4${^>bX=F)y$B4zulp};nv3R
z-F9b~%gT6}3|5>IxydoH@6ePvq0bh$xU)@p=_Bw!U(vHp(^HrK+rG2|3^`%bt%~)h
zJ!nxaQ@?v)Qk5wy<C>r-j=J|bx|u%fQbO!Dh>CY;Uf7!>bYs1_SHk(ig5+gq0uB^B
zml0>b8dJLeVb;kxY@0v55GeKS6Q9oXyWTQcph(Dbq0jS122-DB4;2z5QXG}Hg5u=$
zH;y+=POoM-GVNwzw9TKDbYn|;;^t#AI?Q>Sq(ls!X1(>DzdT30BfEXWxAlMbWH-J0
ze6Fu{My%}XRqww{uU-D|+K$aH=T~~%_PO&o?B244vy#u<<8Y5yJ!`94rjv-&Pk-5&
zF5Bzn-#;_4Qnx)idGEe?8;|9AAGx{m_v7<5fqc)N@A_Z*OLob;?l+eo`YD%Q)Y!{&
zire7HRHJK)f*p7Fs6H*_`g^1D#PsiqRgbexSGn}gx~eTItn)-7mhYaWnfq&zUv}?*
z)wXPMoUD{p_ERZ++Cr8?7MmO_Rn6`wm}{6k|LpIh_^>`mFf58M*>iQ%%v6n)PYhZP
zP2sMeG0iqfs#xOCzj=?hGDK~XEZW9${E>^%u?H?M#OI}a%X&W};mfX?9eY=<HvOgb
zYKB|;$HK!6U%snPG1#rxoUAqV*%XV#J0hPS+4Cntd(vCgzEc?%Li1$VHy9hA`|ck3
z`BuV}J%tLjYXvIHKGcU<uACamC7B|um8*~!kfAIt^RKGfxjXvp?A800{gU7QUgOW(
z%fGj)lv}60H4xtU-oCot^5w?F>$~rC-8Xty+ss+~O?6A3ZSm@;dXqr$m0e%8#CfOc
z`AD2E+<!sl#IqICM7k9J{%zrSDXg?)e<w%no}Iq3(rHR8$(%FWRle@4pVe`}W5EHl
zNsL=VXI<RNAS<C`R60i~Xq%q1@D9I4)h92!xO#Q_G{thSwmY_|FJgsVzTL7qe=cs<
z8s^IL1%d_($~B{I24*DI&Aa;5AXc~Dhc%G<_u|UcOCRNbNx61?!RFqm^3sDndsb;5
zQ=4o3J>{9uHK8TO+aDY5+w|(X#j&pXn=NMqG>+)Rluh#qWDW82yFA57d0*c$3mwB5
z&Nnl6cWU^0GKQc3eXe}6biDa~&%UK+SMf3_A3t^V^0u-lu1x0EuCr~*DNh*IHmvMc
znK~&*iic-UyVn0JY`#kuZaq<Z!X|bxqwvD08BIqG_Il6aD?V|se&rKuwZv`QDd8$S
zYW2xF+S=JN88bv!8x^7_HpWa6VMr2inzm-{hGZ_;$&2l5=B!O<6n<p-xoq;iDw~C(
zk=A#9Y}<5g!I6mR=EBD}ZS(C)_|kYWh4&&y71vaMdH3#6Ywa5|Sxn>ltaQ{Q-ud?|
zxyO65##X1O@$6KYTB9f153;X0k)Hmg@08Ai6?&!h_k<eNPESxx-4L+Fz?DVTw@;Pz
zfP|BczGzYBmd8=oKAy4pyQ*o6w{-ZCV}3`D@mD@v{(JRL4c_SVB}%F*U&M5()EeFN
zI{q+<N%Pa+OMSJcJ_mJ2?kc?g!)^`NjiRs4-7D9dFAll$?^VXm71tzuV@2fVT)QOd
zd1O}l+_GcZ>&@$n6z@B+YH?rp2)ulaUu){szHE(Eb{XBPzTR8iTAR^j5Le|SV74=8
zl6TWxspgYCcCPwiE5E$;y=3FESH=F;q~l!nw_Y7=^AtL!>3T6scCWvl)%k@|k8=+y
z&M{&#JMrbR;G-1@W+B(RZ@EYs7cQB`bU05ww?M>;qxGGlkG<j4`b|n}of2d`*W^s>
zIp1(BlEd@anqOBhiJsNTxDuH0K|MRmJb&w#55W>vMe(xiVZVC9QuK4~xE4ptY_62O
zu{3iwcXLj|oRdc<1W!A3^TKksTNRI3I*&xEL@_#E?s&gXC90)GTy0{Ig7INR(T3Wn
zbJx6#Oszg@E#6T3;Q#&Y*R|_CqjpPX-j3bRmotm=;J%#CCHwQ!tc5QrzFVAmR6M%p
zwYH4A<n`@QcH5@rW+WBPTdFFS@Zv?c_))gCu4}3%7)`yL-S@U`s@ne<I#z5kTV}5P
zC2@7Vmf0KE1Ldr*87+;t>JBLNe|-FIcVED{X@X{cX`&aW2h^P6T2v4x&2RZqrru@K
z)059XJhZxV=c>#lcCOllPg~l1FSoSL`TJYxyxpYjuCrgx>OIS)G=r6Y-9AI%S-a*Q
z)y_?IxiCc~CGtRHu|U(~jHfym?smRy_^HpltG#f0%+<Di+rPJ^$_Jl#%l5Hq*Z!y#
ze=}5Lny2)hz9e;cozARX_ge*3vyN_<{dnqT)%unF3T8*2*e&|9MR@7SM;&HwtO5`3
z+reXIxX@fMAbq+?^|q8I&XnRNksytN{iRzA9_Df^ZoIx^Mbu<n%~|VJ<h(B$Er`|o
zD4#o7C}(BoA~xB{6aBP!oLJQ@{+Y{M`1yW^(4&bSLhZ^kd$;L`glMXIrEd0<Tsu)Q
z+o-~1+uw8bbvw=12fx|-bI0Q!zWPtn_p4sK{)NM!u!qryZOx}hHu0u|3ZZfQH})Ai
z%yQSfKUL7z)AdJ8h*{*$HKJ~*7Q0FhX2=&<2scVEFEE#WT*P>73D=QLdm|YhRiFNI
zv{Pw<{iMe+3-`Vj<LSFF@ub5F(}|lUmKr-&DTbQN^9}BF_N$*QnEK<(w|8HUf6rh4
z{+-mec(?53wc8|K1?jzaTx_&v?X<ng^#KRJo^}6Ku>E9~P50FuDPJGH=-%gYV7uL=
zXs`0p^v{0hPa59z4E8^mvHIrQlVXp3OS_f+T&NfM*>hmpy4|JGlX|p!-ujC<bgi>;
zly=CHmRRa7dGkv3X(r8U;`Os?j*H7}4VoTNV$b+aS46gDN1Saw7kjbN&RyaLHzoGE
zuqZeDxFjxn{j;WerM<bcy_M!{k3$VfO&on+8J4V_y~^^MaHNFK!MPsRwmw(m{y99!
zn{)nT_pYhloRK${SibdQI&sUeL11&&sef-@H(LAb=)e9^*SG&@f^hfMEpm72J-;9J
znQ`k_#4f8tuMGDa9h>{+Oq3?enqxbvIGg!vuNUv>+tV+zdBa_^E=8y4XQkT|ZvRo~
zjy^p1yxF$)?YHj8$}()S_C1_qlHZ+JTU={;@AZazi>F;}lY6%6``g!NZwEQwzY}Z7
zAAfK5`QGD;Ha9A5zQ8wGeUiwgPh0uq=6K$&|9F>8MN)Lm@!!7{_N=Pfc>kx>iy-|6
zrUq-ey<WX;tzY^ruy*msLZ8xbK|bkHw%E11dyjbdf46LSo~^QS`;mXG$ND8@MYpPl
z=oXvx`I@etbvQ;vZKB4_oC~grDV%LjJYADFT2A<#zTo&H!)1!?DH8F|l5Wi2_<|u*
zY(<QMNPhjfy9e%i2JP>C;lx;A|1QP*@syTTvmWfV>fbJr+q0y9*W`saE9OgYQaq$F
zA%r)ELB`o*mG;h+a(7Eb#C^ZJY<;)%R#$VqWbV<rmQ+uJ;F$aSJo2CC?swklDP`%S
zC><K`#PoOF$s>ugkFas(Y*8-|e6VV{-234F2Rm=7G)~yVTCd%!5y>u|t0JCyB}8c6
znj>F%EV+ew&xV=&`*>;BMb({WF1mBZDYQ-K@_TdQMx`su!bh6rY3It)|L>cBq(5!H
zv~q6|k3cZbrVgc=lRk?jf^<%;{%Oc?{Lajuk}ozsJMXl?vE{+s=>o4b%NaMFx~QeJ
z?V;Me^;#F0?{bH;emOF~zW14#j*qOm?Do4eEzi&GUCm@FtZuQz{N#%&g~SaEW(##R
zBL!bnZ2Hu0dhq+F^f$*%thXG}oBy^XcIy=HFB3YN_|zZ&anDKCe|kR0PgPX^b=`iB
zmG26jQ)`T#q@Hy8`zig+d71VE&euVz-RE{zZ4=vcPf;VVzu6}L?vsW!@-g)mk<1s1
zPWbhhFJ9yD@|t7F;{Uxh&Wnx3jy#g&+sN&mpy=^dbLNASQaj_MUff(YEoUlow77M5
zVru$Fn~It3$GZ=^Ca6ZQ{q1$Ir9^yj@#2XW7#A_l-=Y)H<9IsIGhpVX&HttZPI}#?
zB;NIDanKgc8Md=u@7k@a>8@EZ<)W2_Vtwa{6EA%hFF9xI^{OMVYRQ(oE_cz^l1nc+
z_N@zB#XXgA3e)6fS=sA<-hDI94RhR;T-3k5>~*y6YK6P=7-n2>*Ilw`_S^jGTPv6o
z+rHYC@*hhJ`W@oBx&EN1--45BSH21c=ydygon#kP@=Dsu9DU}O&>il*pDuXiJ$?9o
z^Q78M^%L&$zc!z@O}tw%&3m=g@#|$W*4qNkD}MCi@H})w<VFU2o2ydVYoBdTTQqMy
z_~&F<7ZYSQ$+@Q8Px)33FPDzY=1GkV`^2uC(`mdDe12Nni;qFO9Q|h~b@ywurECjy
zQ&0^^al5TF|J)hBpvUv}w!Sucyy|!3Wb<rog;lE?Yo6ANP28wxm-7F&2b22qiM+d5
zvv><0KT9m`E&IBd<D!K736sECj%7*@*KT#~+*CE|Y*=GbjYFQT)Ux$)Yt8e&dwo57
z_3DoYFTcvYbxf}1e<QcRY}WSH`TKV6U3KCEW6ZORX<ba~_xf9AAKn)?*-dQ4E)xU6
zIbKq_*HZe;@Af7fSFBfM+%Q%7W3|Mg{0b(vaKRGo1&&v>E>BR*{BF25-9yFxO-9oa
zp)8S0CVX=~<@Cn{UUSI~=9JmWs<L69TuHT6{uM{VuahUFh&Y5@%nQ<VbeA`F&(S>n
z<b>A31q&v3s>~^$5!=tHzo$7{qTHp{cJV@)ZS(V<_f}=zzahUR!%VBbSwhsL;LEA9
z6DNW;v?v8_oTkab!`63r(L5z~@ymPvnTUpkZ&~Mh?{?@T;mE#1!>UcMd*!$6yq{b1
z?$*ufdmlm{hi)tVX_#^L{iF~rweAykdM8dKycE%4+WTs4;>M(h$5qpWWlyBoWb_}r
z;#A70Ud-Zt&r8%VH-EOWoDILk+WM7$l~v1}En5QoKYv%8w&vCMpc_A)%~-<p)M4(Y
z^oniv)+&GNU0&Z+QST0wnqsgt<)P5k{CyJL3X=R5<@=lu&u>)=?!U&7n;YUMIXR^#
zX9Cv`B~#9%+jEy#oL<OV_h1uWu0;8x3)4ykuF757{Pz3@oBB5Ida+p!2?rFe`koN0
zztR45(w<fE8mGcmmelNh+@IZi{@#(bQnIg4?rT-}tz%Mf<l$b;Ssnj7;{F$9+)&w~
z!O85D7|;^-B%!BVKvhWk?N?)g{~>(3N6s7yn)E41qbEZ$WAcTzl8+guDp_wbM%eG*
z+SIl%ah`V=`|o`Ym)4eB1hM|~Iv#L-!)mEx7dq;jc?IOMyv{mboaS-e|C)@cThX~o
zcC9?#mo2T>tCf%1<{6rbpYER^^E2Z7soP(F7fpX+d$7B0>ID|Xy^8H?vUxgm95z0P
zoyND<GPNfm);?jOyuFs8bjd>7dA_eTPMr2JHH|L6u_-(G^xk~|xwpmUuBiWVHZ13&
z^3qb_pdLH*df~29dYkT>U+R`H$YT9^dvWaF$Gp9LU#rXK8Z#SRU1oEBUFx0nE*mSP
z-pHHVGUn~Lp2a4k75_My$K9iNE_?EkrD@wZ%X&Ag;O*vT&Ro{z61)G&VquQ5G`E&{
zPIsO<dn{j3vh&o%PM5Fp$HeX?e43S#GTUdV++`t+n<2u=QQGx$o&KD9bbRsJ%sKIL
zm%8pwpQb4(`#QbP<-vzIrPtfe+P%`{s*UH|RsZqH!#Te~|GYT+b^W8`5LB*L$DpNM
z@@?UQ53MIfMWdHwEKzEmasIUE*KA+?*gr3h+iqe{3HlRJm0QW;bCP+6k?f2h@B5cM
zV(sV4beo=A&|~TKxL&2}f#rt@iJw30I;!P*BWmf78(|gK%595x=18wI;oRdfBXXz8
z6Q)*{kERu6g;K7wST}f!Jrops*y#F=qx)Ik|09Q9?7PXN@FjZ2t_dvDvt8aFzVXdr
zdgI3ZLVxxP{So*4@Vmp2gMZq?#T;%=t5z&iO13Sksebk<$yDNIx76Fj`a8nXvb$LR
zKg})6sPQOuUc)K#a`P<7hcR7k$!3dnEpOa<@j>12)`ECbO;2AxhY8mL!@{(^^ti-@
z7kg^`oPN<x;%&U=o8n0~j1n{WQzpxFvTXBlQuSOZ5!{jSIN0>NhqT?PEw62hZtOlL
zVGyTX_HR{PxQ*xXgFjVRj;nX+UatRmg`<DJ{JSk`b7$|dHM_XB=gsz~5sNK2IC*5e
z&-pBk$=UMN=l_EggNwiashpj5PW|$h*sA1-8gKI6Tz06BVEUM-R-E$UR;NiA=X$5V
z4Q(sc<=urlWHR}#Pf(62)>8N>oT9jvhht~my%V!y_^+PR3raZp*)MwYM(HQnM_=@x
zsaLAgT`IkSr<rM$P?Ogp5jTdfEGZ`%TlDSzpK`Lxo?+pprPjB0{_?dFvzL5VTkfJc
z<Llca_1koo2u4*hOUx}eni;gspo_=P^YL1(FWTIZn<v~ma>Px_Vn*r2#ik2#ZstXQ
zSx~IAf7660Bh#KqAycO6_(g7DT^>}PaPt@Eq~I6z7uO_D+`4{lO*3;vd+>+ChcaPy
zFOC<-9ew`HBWW{d=i>fJuOj)Q#3mO1y{6?Az$#%ZS*{gh?7rc+;*@6@9~*4N(uF>m
z@Oc#E{(dH>vu@tW0{(q-YL~3NYj<f|r$*2eCT{k>N-T_eterd?I!n)qeAGT1#yd&q
z;wlymN#kWNEb4!(cbA@UX{N)8pM`JgkMT%rnc0Lb){#45nb~vY9-HzSKg-*bwfpw1
zca)MnU)ARrw0GgmIp@wzzTtPP@W6U+#>HN2>6=ceO*EOM;8fD~cw&Cego4`&H;<=G
z==y5szE+Y!gI9r3qtTyriFm+~lb>Du^p;n-crIXnnf|!BgF~iHUxY_e^#7KSO&nfN
rk37q$-T$U6F2!Q@=F_of-k0#bR`l$B@A&T7f5ugJ*nMWtW?%pSrC}1}

diff --git a/examples/avl/tables.mlw b/examples/avl/tables.mlw
index 5a53d732bf..419f026962 100644
--- a/examples/avl/tables.mlw
+++ b/examples/avl/tables.mlw
@@ -121,6 +121,7 @@ module MapBase
 
   (** Extra invariant: sequence sorted *)
   type t 'a = { field : Sel.t 'a } invariant { selection_possible () field }
+  by { field = Sel.empty () }
 
   type m 'a = {
     domn : K.t -> bool;
diff --git a/examples/resizable_array.mlw b/examples/resizable_array.mlw
index f70bbc6a7c..b7df81a634 100644
--- a/examples/resizable_array.mlw
+++ b/examples/resizable_array.mlw
@@ -52,6 +52,7 @@ module ResizableArrayImplem (* : ResizableArraySpec *)
     invariant { 0 <= length <= A.length data }
     invariant { forall i: int. length <= i < A.length data ->
                   A.([]) data i = dummy }
+    by { dummy = any 'a; length = 0; data = A.make 0 (any 'a) }
 
   function ([]) (r: rarray 'a) (i: int) : 'a = A.([]) r.data i
 
diff --git a/examples/resizable_array/why3session.xml b/examples/resizable_array/why3session.xml
index 0b713f9087..9a8c463ce2 100644
--- a/examples/resizable_array/why3session.xml
+++ b/examples/resizable_array/why3session.xml
@@ -6,7 +6,10 @@
 <file name="../resizable_array.mlw" expanded="true">
 <theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="ResizableArrayImplem" sum="f6a8ce6d35230e1f00a4648b2f798bfe" expanded="true">
+<theory name="ResizableArrayImplem" sum="d62174e0e2a371227338667fe7fd890f" expanded="true">
+ <goal name="VC rarray" expl="VC for rarray" expanded="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
+ </goal>
  <goal name="VC make" expl="VC for make" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="VC make.1" expl="array creation size">
diff --git a/examples/resizable_array/why3shapes.gz b/examples/resizable_array/why3shapes.gz
index e3c59ac438d704d3a3c52a94cb770e0d3b80dd85..2c2efd6812f20b819e22f524e463b47af321f4bb 100644
GIT binary patch
literal 2498
zcmb2|=3oGW|97Lj^B<oO-1j;B#hiqOb+60~;tp^q9B7!Rtbb5$Rea|}+4Bdkv2FhO
zRntr9rbzTO+x|6gn|U|7hLzWce!Uv*dow6V$1N+Fi-Z4CTMFmq{v*j#%>Ldtd;0nC
zvqm|&7yP?+>zBuyhktqb?)8U<^83GCI4zgo7hm&6_3yOz|9Acl=fD2=MySZ%JJ+V4
ztzLBFp3k@A(u;QFom*LDcz)%x-QOm!d~0%BpZ&0`)@tul_rzJJ?K#ypg?;HyWiOw?
zJI~aAmB;yebe0|Yy~Xy-=38}^tMA6m*Ngvl_0#3|^X>i~bS~Ju``%e=+gZob?QD3z
zrpe4{|MKOH&9Xk@oM?xn_p5YE6Si)YxH!SgLC^Ii^Kn)+`3n(Uvug!%9yu?&d-wV8
zvyboAe`YB;?{NQ01J8!%D^zbvIBThTPn1!N4z~<kFeUTzQ^n)wzrV~gFt@$!&)CG>
za#YK1L;f-LcZu_oKOG4!+HD)V;@MWo*&#kcir%?`OC~?zy{RxYbZx7hX>v02UxSZl
z`|m7SwLIjn7N?*2%TQ0P&urd|uX}<uoZPxJSwxG^&DNhUU;a8atns&c%iGTncTAY8
zZ87C?<DSV@8mi4|0&J#S9|ULo*<-<ce9!sW<$QtcM;9tA4?ZEb<(Ps}GOI>c_>(0z
z%@@2Yi?{wWZ_agJQLEUpAa$DEE2T9H=CHCj-;}VtI+b&hW_&*zzwq2A@6Nv3cG>#b
z(o>K7o~3@>QT1X~`(u~er?dC%_W!B<-~LkVk3YX_t7=%e*;n_78?mGuoTMCHki6&Q
zHjD0?tvi^0KW;x6{B!%=#|J0Oef0Tpd;IFcxajry&oYk|R+hze$xjdO-MRQ`*rCEg
zRx^`kCWEMg(8Lcm`_`_PHa9H!m$p%Q-p>-{*gm-#=Y79$xlFj`s=Da3K#SUB1>4J8
z_eTDD^R458|JOXP)-_w0A{8_GF1+zoI3Te(MCW$K=HHLKpDq30F8A(5-FL1B@6IZv
zs2RUyS*f<_yM5cuUGH|El)l}}Y{jl9rfD3k->Sr^b6V@Q!KUI|hSIkF`l>hkrIze^
z6md)XVT-BiWbG;50@JK#ojEvV&CFXfZ8EO!4$D8NxMX$q!RetcFK0b=*nXMe%P#SR
z-K(4;WX+jFbDMTnu5$m#;BOkHFJ5hsvo31N%r#eD3Gd*U^|ti+oPLQNbJ!gOyb45A
zmo82)dMdE#X=ZQ!q8&^9zf9$PVDN2v$L8dE$vri@OI|qz)$rR#{A*E-;5-`jGW3+-
zW<JBz06ETEdyjlP9A8;<_gwMb94G&sc|{B6Ms6%?c$#3_dAi@n(3|b+?YHOK*9vQj
zEG$vuJtC9U{psYbgJ)wneR$5hpU^YhS?OL-cC+Ke#FXaeO2ShVF3n42?XK(4FpODe
ze4tm{J1Y3;oVi7QS1p(Soc%UwL23LN%V$~n`_3`M{;u~ZyK^n%?(bL88A}EFI>NHb
z?(t4{4i^u6wMQ^vFXLjbur<QnX=xp2gr4wRpHp1>XovAmg<XLK&1<%s+>hy%b2UF<
zFU-CBz@viG8p`b(*ri>?odg^Wm2c*Bd7qOCikWTf5^dB`vC{C?=8dsolF{v#7oECc
z9J=hH<zBH5)*cH&{EV_sF9=9F#3$CP%erG`iTI6K#y3oMzL;aQSJw6_KkKje|NE<4
z6lYD+(0YAxafwLKrZW|5A`DrY&p!~nW9$+fuqJDJ+=q^wyXHq+-rCJsS((51+r0<3
z(zte5W*u<~30b!?Y|*z>i!zrRuX(yOjN$0f1>E12tg<wNKe=!v?>wM<Uw=j&gV?Ud
zR=fUIyJptM;n#PpDl2gmb6C73{9e<Cqt@D+o=04Ivbp!A(eytOM|VA&6#kIGS$2lX
zqz{W4*k@`a6fuP;Fm<q9=vy>zU(LzyD_bYL6<qZ?(5yzH&D}<8qA}mc>%M1elk#@t
zx9v#XB-NriU(qCr)tc=_O6H#cOP1qx968Hldiqv&&USvwXi(7;CE0bZGvSfsw!7v#
zci;Xz`R=;1qNBP`60e=A7Y+?i{w2V4-+6<Cv39MITk1K!=4*?X4}N9oh?qX5yGU$V
zFjvI1-lacgxx9+-b-1(c<GR24dLsG%*F4($t-AJw!INtj_j~^}x?6KM(C<L(?2=>6
z-b@jXqkV!ro_p*0#cOO@=a#YXcJ=isfAaYQ-bpo!3H1iJMJaCSG(4%`ti+-9{P~L7
z<DRE(Uh{eOD~7XX?%Cgs*J=+()e5uD<9Pjg<Fjj@gg1UVTTuV@OxC-DVVlKxH=lU5
z%UH&W%ZNpJv&!<hU$1p3HFOKU-pak+G44!gsLpRw^*G+MClu4(SoS<na@%l#W8MLd
zb4ekUi@0ShrnU4dc^+1s@;_$VP0!U^Lhi-rU0lD5VXgN6Zf=1oK_cPOPrgkksF<nI
zeZuYYQvRdu8(rRidd%myym(`6)j6L-fg38K_f23c-L#=)MO`a{L^jjG&_=5zit98F
zpXGlSec~`*_DdtjK;B=@XLcQ1yeg^1FVas>leux)lAVDcJf}|TY@N@b{${6@?97u2
z+UZU@W>N1Jw252Hbe_mvBRKD%nRHdn8UD30vU2$j7P5bj9nIH#@Wi9OcjAh7lJT25
zUrm?N*Z+FB-(RE9xpg7O^1T6iDo6kCm@5{w<?HD`)<PTC*nRCjWX|09_|@A<{0<#!
z?rgf&wz_JY){dkLbEX!^tiM|JT)DRN-HQJcLhrA79(JOS_vkC0`zG76pI@FX{(A-Y
zlTFHtTb|k-;L-ojQh9pn-Nm{WSGqB+Ir$_v_@r^nUBk5*1uKdVE=*`uuw1oC%Zo9!
zsb-$~E7tw#FLpiL&}N<cZo;A`0gsM3vCFS@58ZSA)b*=e=Ur9a`?;9P?+>xhJ{)Yf
z>z*msor^r%)4i=f-<zgY?a{w&>A@2b+SiqCxa2&&TF`V{b&p-&tdNuCqFVW;oev%T
zkEomre6cf8o!w|x66gN8XX2If7l)tx&C)Zi=bm+HiKbu0!sbBF6Y3MH9&g$EscrS%
zhhq0$1VrUMGh|?~Um|Zj#k8+_<HAqXCE`toY^^o!*cpneln9CC9*R8Py87{>qbgf!
z7nWPE@4nbM`|^q{Pu-?!-!9Pe@LDNgy!=k&y?@hqj&EHw|2N;!`0bf#nf|)BAGMv#
z`talggX`k>`F=Ciy^WXOE1A^wXp+9eDxI#&%M8>rdz(}zb(z^}GN^UMlv}@N-^XWa
z#H(83#Q6QXAG@E;u{I^OwaK%$&tGSen{v-&#@tTTbma);)b$shPGHV>IK_i)=A@{d
zWy^B*d)KsiNZn)q<#VvoC(L`cMr!gV#cNYyZl7g66qmhVbI)J5g>QmNBA)~poIa2^
lrS{RaJJX&pw%t$J+ENznw9h`L&%gXXbH$S7x8sZ$7yz=W)${-W

literal 2433
zcmb2|=3oGW|97K&^PlVx-1|EG$D9O)u#by9681C*E?{JK>#ODb7VyWb=S>A$S-!#S
z`1zA|s|M<By*;mg&D+Bgy4zePu3vSp`ly^qO17S22=kGHBFEJlHhvN`eO9vZ?`_w=
zHT54m|HuCLw(eft-W^Z;x5xkH|NmpE@%xI^+qbm7KD=H2sZ%Vk_;k<Q%wki!pV2#i
zKYthhsb$u&Pw(g3{Z(`>*t`2ytpDNPD?iTU?{|(i=kaqct0|K*ZZ|hsE&YA#(Y5*8
zt}sTr&$zI$^njhZ?4n}P;*J*`ms#)M|12;5a^Ht{-#*_xdiZTU`<A+$cUCP~7wvFm
z+2KiR(!4aEMRkYWG(PoaSxVm=?)aLW`Y%7n?t8mjdj8#2iSicC5wY^gExK-Rx0Oh1
z){1EEy(y!A<<u>i)XAING;RqseVf&s+;wY0Wb}*R{Fs{uw$*?9+J9$BW_)I!S?09a
zJj>F8Q<}FjRX*ok6)_>W@8Xi6Q%9$t=imKQZ}ySD!k51NESR(M9IMQ++b0fYOZQ&9
zXr$3DCfdT%SsI}JV8*w~zvmQREvO24liSyNAgV`;Gpu11+u^v^!W?_2n2W!zH@;EU
zV;17p5hgA>X>FIt^hF9*dgopShP!zjtFrakQGYS;ZJd6d^}gh&Rd#POqOOUF^T*~r
z{IKZkPt*JNo_-4bC-=gx?%!WM`#nvq%#z|$`UF>BR_$!E7LQr@inF^vlkwYe{^TX6
z@^`oYbuoGN{5b!9v&WmZt=&5>ZZ+TO#hIFk5pl-P_&2W;oztOx!bMnv;V{oW!8V1*
zv%gh6Rcq9XIbWunZ+FilJc!|8@$@D}QPZC(A)i<mZF*z$B)zTd^)tiWmI_~j7tbzE
zy|g4irfDjV?m<^JpOqQP+j{lO>T5JNefj_4ukQV~ag2AO&An$9&icxf8F%Gfy~pOI
z?|vIf&8}sz;x`Ok+Z~{Pe3hg}j%cNiP)t{X--nO>=l_N`hlKBqs9wHDDV+QFsikhN
zGh1#PDVQX!@o3+ddtb{`JAa96I=gk!X|=^UrwbFVpJsToNqj=3Z}SGr95$(3CfmDr
zdLGHmOIs7Gmv``F$=OABEWBUaIi_65U1#;)`H)7D9HXP8YUGq&U#}A(K^?Cy%iUKk
zJv{%%YJmfFZ}d5rANY64{b!oom6=O_$ki$QY%!hG=C!2xq-x?u!>3GY3Wuxo3x9kF
zuiP2CzW8?B*W0t#SMw<NuDQY1pc2{t>C@tXGjkjdr+xmM_&TI7R5JPo6L))%siN@L
zL^0I@O*?tTS;<9z`yRaM3idSWOcI#b>1KFaVVjeWy~-7d^RIb49;;5fW@_r5e0Jux
zXKQLU&*WWmcY0Lc&YC&<)-v2awqL*O&X$n9yl1y>2y?PfxV7VErnyr4KGDE;O~DQa
z8;!S0eC)i+Wvr6O`OVMddB}W=H$LY(@(k`QxUK7JZoZiPGVibRN1D<i-sDT>q|E>3
z;8|+uCfaKtBpP1(?a7S}GjWd)?iD5L469O-XRYSh`qCs=(rTfR_T0<ajQg8;j!jw9
zt;*QCS)fd%Bt+Z8_~rQxTSGQPKV1}j?n_$7m2KiL_W!s4(ve(bT5Kd@vEZ9bv09={
z;Tnm>htofB*clyJwJ;)M``nKmal6-_?=-8i2>kq5Cily)3+tve%-`g8*2h(NR+{Rw
zi=k`IUAFxA>6TQ(tKco6Rf4nET(e|PYhF3;;l%gmKK2aUyPH~Vds}TATOVA{idifh
zdqwnuq_mGhz(O|vRV*h}PcIBO^?c`(;}+Lcr|;=vuy}VMb!upUDAS8Gf}6t=l#CsU
z8cb$X{rj}^&QsHtjP46D{M#Nn+uJ<2IAczt$G*6)cib<3{q8HU-uEWYp*iOT!lGEE
zgmUI&{<y%x(q6~0!q`q#|BA}lg}e+B%xc*(>hD8KUb5V_Guyd)_GSIuk#C*^MV<H?
zJ^M#*$lacswOlp)2a~iOeYt5Fyu?aIXd%0571NnV-mfC9xgTq?o=Hv4+vhgfY6a(t
z*{b()|6G;)$ah}oed?Xt&h7iQ@qL{8d-}&`tNXm!Uf$YL&R7$sAUEG2dui>8rB&5#
zDYe}f&TP;ByXt9ub%WP+iM5wrOevf-Ws~00HH-UZD$WX;_xRghk(D90vkbRC_Y%03
zRVNd%dwqO%gsWp*%iFIDcCP*Fl9P1#{(ZL1mF4!=SBZVizj(Ivxk@RINQa;J*?U!7
zE~~Tz42AZWJxiY;UK~34bmGa*>9xk2&P!Ug3eGvoktT6aSmK~(&n%CUK%w@C)+L+D
zloozEFRm3gdE+gX^0-CuTN!kx{y)mZvNcROtND_g(KmawSF5@<7fB}Z7EX8(TY2N)
z$JaGc_O{|`6Ln_%jk4R!mb<Z|^+217!B&<g?#5fw74<X^`}5mvoA6t9+qKk|MUp(f
z=X}-fpVcO4<s1|f<<7SHrq^PDO)Ix<kg#WsyQn$W?@&rWPq|^Jmx^r2e`ddlAtH_I
zwK#6PYm%2c^*5^bTmO0o3%S3`z9rZnyg2cnkn+_##(z$zE%`4S^gd=PcjgL%u&22J
z$BySb>ECks)T+||ldh~1I+0h_-Bb5hpdv7TzB7xP$n&r@rHfv*`h2;%&^q&>O8o4%
ze(t}XT?zcZZ`Ho5=XEE@N_8ET+!uXQ&v&`LeqW&YP4V;RG$z>{_-g-8lTYQ8+=Q%8
zX-gTVrF`19@`>cacP(K$6<d}j=|>o5om`c)%J4wz!a2`6%MQMm+_lbr%|yRwt0hZR
zr!LvJ!BB-OBa7o`OW4{EA#SJMg&1A_c-qDNv+>M%{p-rKnaXFl-P-)q=JLH~db{=e
zzs~&S$+k9TR>Jgxwd;Nf+f4lM%_6Hr^}cFIqt5Do2M_3|=tW8_NlfRr`svkk-|yM_
ziQ5fl$T+b%dM_8)Q@AZ`ebc6kGuM0(_Sjo^E6(Nc_KP1jXOyh)oK@MwVEE;!I*;o)
zZ~bf9^$zuFntwJ=K4dTUtf!^#QqtUlX_XIe@2N24%#D+{t9Rp7&a`JHlHQkAbZz?j
zyeX%rbEU`0xli8auPlhM`nB@C!KbfQXU{x0{=BUs^;Fu27bh65dhNHHXVh=(JE!Vy
z<~lc(_(n6=(EM0YzfEFOBUC19*k>}hb;Xofzh~dar_05g`sGx^m+SZ3G;I#H38!UW
zw#v6(Yw`NTo=gMl=~<e7o$gu(7wB(v*>FmFsw|i4+N-xXZ`Mu!@nz<f|8f#s?(znc
zuTHTPf8Le+amu2%?|2gRZ7+Bpt6LmUX8CiG*P4iuDJEKq-r0Vp><$0^r>vEHTgv_O
U-v&#YyMOslO)XF?H)LP{06cZK;{X5v

diff --git a/examples/snapshotable_trees/why3session.xml b/examples/snapshotable_trees/why3session.xml
index c80d9ccf8c..6bdac2923a 100644
--- a/examples/snapshotable_trees/why3session.xml
+++ b/examples/snapshotable_trees/why3session.xml
@@ -30,7 +30,10 @@
  <proof prover="0"><result status="valid" time="0.08" steps="777"/></proof>
  </goal>
 </theory>
-<theory name="ITree" sum="7cd3f8370a8f73c6e8eaf6684fb82b17" expanded="true">
+<theory name="ITree" sum="13f9be3f8d6ff6e1ef40a222286ad984" expanded="true">
+ <goal name="VC itree" expl="VC for itree" expanded="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+ </goal>
  <goal name="VC create" expl="VC for create" expanded="true">
  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
  </goal>
diff --git a/examples/snapshotable_trees/why3shapes.gz b/examples/snapshotable_trees/why3shapes.gz
index 85763b9c85dc13fb927e93d69c0f0961b298d564..74a0e8dd06c106a3fd11b398708b1df3579262ee 100644
GIT binary patch
literal 936
zcmb2|=3oGW|5HP~^KX0b?0X&lWY1n6%lrkl5_zl=9Gj*ejbT2Qot%?nzO8H9|2p^n
zi7D!iw;9})DE^%I`J?ht=QPQsQ)Z=hFR=W0BJvuikuyu>^KIonOZIsm&u70S|M}nX
zyXvpv<t`UnElDmfw3u7}!{M&w(xV6RWD>Wp72uP-F#YiLchBcHead#P^02p3pQBU3
zzkEi_&*Zmhw|igQu9<t3vG~>dpJ%O1-D>p%SN~`$*)U5|TBS&@rIX=S#tBAYx3fV@
zRp$tozAU`I)VOr{=c1WW_a5%wouwms@5AQm=bt{z?z!~*vf<X;!>&F?iE5HNM3uO8
zmt1#CoZ=#}FzmO>^m%%#{$D@3aeAxrujhYs*Un<Sa_O@w@5{VB`^2~1I>vJ1NK0R5
z@w_Fxnx~XhHK&|UP`u96r<$F4QmQ>{`@MO6wa@RX_@7O&e46rGuJn_6>0=jbujTK*
zuQPh|;NPq%+XQ3S6C;B(StnLbXpB5>^VGvpBlFeOKTE4^mM~A9pUfv__Hml;oEtJN
zJLCJl|2}!)x4%VE%}Tp7om2m3m)k|!^UVuAzv0Z`d0unR<=mUay?GwD@p;xaa$!He
zGAxK=G+}V;cw#y+?4I=N=7hZ}6Wdo9oG|qld0e()hIPcGPjStUHMh-fKlLQ-M8|h$
z$K*>!?8%=#`u%>jYqs2#w2BScCD9j8-;G;1Td?+qa+S-@IFYBhT>Ac1o#DwfmX+<|
z>^lx+wm6+i(MaK#))VN)sD0_tsb?8MD|Fsgf8?9+#(VNXgPuTz=>jLRoO?t+a`ww`
zu<VX=yK5w6+rfO?O#5wbdhp&ib!)brv@2L_d_B-v=V_z~TMd_n$MZGM-nCxdsGTtV
z;V<DEE<9FtO`m?htl54`^s(pd8%hG}D+5GazhoqDI^nfzj->IiB;ODfqXk`>MVYMy
zKZ;Vb%&%W9*`0U!?X+3H*gta}3z>0pNnYZopndaVmZh!dIjklXdh~kK;Z>%QTa7L&
z-;Td<WlF8^&MgyF^@ZJEt2%LAyq%$3C^U8P>52Q|=K0;tJ%0L+j_mx1M{jN1-<!J^
z&OGpZhU@-wOZ8_xPQ83n!qy}0@uG9(cIByzvAK6|$LufKb8p{`eW6PjwME#Q6(i?4
zRCh@lq^)d8Y52T-nfLT{`#(u^7^}*^w3Pk-c3zmg-0xo==ikj|sy=M<(%bK|%JgT8
zOE~ny(~fBAt@yY4eY3>(AFno@c)mlFdDXGLxh$pjH~$r-w)}W=^AEpOw9uI=oD2*A
D;w{vx

literal 906
zcmb2|=3oGW|5HP~`=!l!_MKn<Vdu_{E7Bf(ZMPYDByM{zeC>38-NmhQx2k*mdcRt-
z_u0c(<(Evyyp(=U{PRQNm9Xat%jqhaES|c&Q&c1s1zjFUZ@#_cbgA(9`+nal{Eo}d
z*59_@=J@rBuIKO43Tpm;IazjHBAsz(aLeCyP7)>w|1E0Y{`<RsLCM;T`H%X~85}mg
zcUjeC@_&!rcS~7or(cWX5m5d&C+}8A(pTGP-8a(Od#AZ%o}U<WEQDc#m(wQ+Lk}Ts
z-G5TK;`94s_uP6{G<WjKhjahk3`y+!&^P~Y^OJ|-l3Vx3pWB!#eah*H;N++CvW^K&
z?y+9U!j`AYw&LQx8`1vL*Z!Y=aN_ov%D=CFjgArF&dH9?FDxiu{?&H#RkKshn_5l^
zXfB<YEzf*@?U9)UoF+@84p>&7RgHXf!}Z$k(>vGyX@An$siVx3FCTckeq%mQw)g8V
zU+;yx@yJ|TvW0i?C1c-39Tzvd*nW4hew4#?&G=xb@7cS%o(J39{9}CNz!|lBn>&?f
zJ15IMfBv{o<jXH*KK<#doOz;O><?eQ_{--7k-sIMRa)GVSsr-1|Cy8Sb0^<o#^1|Z
z>n#~N${BbY(sisd*NU9ed~2gz>#g+Falv!%c{v=r6_c_O%DjHd>8!tzH(zV=?Ssm4
zZ4F(QZP<@io_rY*`u(wEPJ46QqSsyXimTh#asArhp5hp(-&G@h_Os`?Z;Ng`pU%EV
z;sC4PWCuZ>M#ZNO)=oPmH0gJT<&uQPiC^PhKGS<Y`(}gUZCB~3+b^10iX8VXnx{2$
z1&>hErntpH4;HznrFtc4wd|j>o2N|LNb=w@nTr>gy!apgt~31hbZKtMx~-G1a7#xN
ztZ=^Kv1#`djzF*E(kZKL7i_v%lr~keCc5+1TdP@l_j7mul?kp7c%Kl`D(U)2PVMZ&
z(}AgLZaW$1OueK~a?>p0cH8w${$D<PQ#UcKEM+-Ws&Mh6N1%0|Ky885i-eV_Qy1U9
zS+{p@%&y;E&jV*@+ih~Wov9)x?j9g_aOs4I{WEu-wsrq}>5`(w1DEz!KORoken06d
z)86l2jgNj+I{Iy~f@p@ChQ^n`%N&<(PGE3;)Kti1QERrV;`Og7-HLuwYPPNa_^15)
zrXOuDzWWyi{eN_l{n5t#KP>!f^z4e7KWr0HzV@tX)&7XDYt}q*-Q=OZo0WOdt!Z9O
Z7CoEp`^YI;Wt#nG{2BaJVm>DW0|05A%HIG0

diff --git a/examples/tower_of_hanoi/why3session.xml b/examples/tower_of_hanoi/why3session.xml
index a8c81d24bd..95f6cb16aa 100644
--- a/examples/tower_of_hanoi/why3session.xml
+++ b/examples/tower_of_hanoi/why3session.xml
@@ -5,7 +5,10 @@
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../tower_of_hanoi.mlw" expanded="true">
-<theory name="Hanoi" sum="ff68094fdd8f1e3a29decd895f45d1b6" expanded="true">
+<theory name="Hanoi" sum="934ecac9b836a8bb7eba7c149be18efc" expanded="true">
+ <goal name="VC tower" expl="VC for tower" expanded="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
  <goal name="VC move" expl="VC for move" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="VC move.1" expl="type invariant">
@@ -97,11 +100,14 @@
  </transf>
  </goal>
 </theory>
-<theory name="Tower_of_Hanoi" sum="d2a79fec40fb0761056b76192fa05ccc" expanded="true">
+<theory name="Tower_of_Hanoi" sum="f912cddeaa5714ba310fab811694e537" expanded="true">
  <goal name="RevSorted.Transitive.Trans" expl="">
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  <proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
  </goal>
+ <goal name="VC tower" expl="VC for tower" expanded="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
+ </goal>
  <goal name="VC move" expl="VC for move" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="VC move.1" expl="type invariant">
diff --git a/examples/tower_of_hanoi/why3shapes.gz b/examples/tower_of_hanoi/why3shapes.gz
index f306b52c959c2df386f27b01bdd443130efb88ad..bd5aef67bb5005023685704f3add8fcfb2389e2b 100644
GIT binary patch
delta 2489
zcmew*yiR0-Y`tuNNcaJVjq-oDPSAL1b|5ck$-cLD_uKc``n}m`oVm+){l`VTO&5FO
zesn0wPx9iQDNqzXKWl~U;^z@XCpk^GMLfRx>u%`&y}NJSsmm<?`T6bLWmmWUe$FsO
zO7M!)-rX8=lAR7-@OGK*RQ9`W|NVa#?>&7zyYBD&)%&0CzP*cW`u+O5_iEzW-wN-u
zt<rqG<Cggv#$|l@--VfN_W17R`~Ln?;PJO2TV_A{>$u!>|NXtu-~XKcntz-B&a1m=
zzc>7TC7<mOefQgH{pVsk#S>)T-@ab=?O_$ijp)pdwG-1-wBBrKm$6LF6L^^Q`M&?#
zSHGV1*ObrAH#;wuT$<-=vaf<Mv#j3w;XVE?5$}};3|HzOEwfR5@nRDvC+lV9pt(19
z%#Zf#h%}w5X4{dl$@!wP_q#XQfr2}KmHe(;yxsh3RdH?gXHly^r=En%H*PU+<hy9P
z%q3FG>)8~qt6LQQziC*n$1kJsX>Z%JCE{lmI7UxAC0XObq!<2w-_GpF`m;~Br#Zyl
zuh02avvAwCpF%IK*G({)tyy-|(%53Emz#Le$7L5(L&aa;v-v+OKX1MLJ=4ASWc=HI
zUXJ~JCGVBokDFQ7_T1WY_f37@?nmFkXYfi)b9b?lD>AL#eR;~47Yi(23Z36~z&Z60
zr(q1Q5Yse?jZG_!H~zRM)cWS^rj6Wd!Y8xtUgeu>tY^PHbAtJ@b=kN4KRtV&<-hvu
zkN1bKeA{lSS+gVjD8IEy82|4z%lX)OrZn&6&-b6K!K7TjE~n}9@xO_A%xbX=B1hbs
zqIxD7iJVnjdT&7zf3FkgURlS&UBCAJ{9UB;=5#}=f8*15mNkuDOY`*h|BPvvZ0YfQ
ztAzXtmVlTVF}Di0HS%4H>bZ`7;ML&U7r4Z2-IHfRZiOq>t&n_tC8$8vu5L+B&714{
zMc@5+T4P+cwxHppWyWvrj~!8uuDo8L>2p}##5c@*-~Z1NpEZv$TWKD2>|OYk;f3lK
znN3LxPB=D*Z_O}!aB!DC`(ekc9@A&}emi%_XuYA9v$2$vM^N^M9n+nDaOs;mxALzP
z`!VywvF&_ECapZ(SX_F!{C&O3WJ6|g_JRX)J!&y3ll_@xRo&Hl!^PPjGn~xnKl*yo
zu9m2|f7!1us8Bwm_tiDHq$^<7Z2K?kCr@OS66*cnz4=%BGK=1l3r8-`dCv3k`{cdM
z67`*Z&pcu|nwSHFkFQ}&S`xC_@>fIBs?;>i3SMu8hn7YanHP8y(!KX^A9N_WQv1F$
zNXmHA)k?iuM#XadSNh&5KJy;zez{b6jfCxNMnkPT)l(k4J@dqF8Gk9yDe=;T%FXed
z417_Eh0A_#e0FQj%>d=fl@T)zNF+{+ovr=O)nP*Y3JYVF1ivF&Zh015bXWZ3C}pDK
z-rC;3{qJM5(9$g&lHxX-&sqyBZoW2mdvX8s=}&ZYD<(`j|B0)6-*n^Yy94=V{kih-
z?@WQo{oj*UEbR84*jW2bM~rz&&c&4F>&_-IeK*yVtXuGR|JK>{xpjB<{@-xcUhXUB
z@`QP3AK&e-HF;1U`26{bMzi}XE9cu(uiC2N!80j(-HC-yHyzpiL}JrV%L-eC5Y4z=
zD-l&4wGtj3xsU)ZB`sU#76bd|FNGYW6sEj!nR}CS{o2_JdG0>iCzcduxNU1p-weM0
zn(RLw9{+b#LC&k&&Du6NUn$1%O8bl5-?v(D_umaV_^Qx)*DeDM_WDgT)>YlFDt7eZ
z*0fxZvCLF0yn4avm#592xxYVuYPPA2-44?k-0PV*HnuOzX;~Y+CF72~!nA<E!;4#s
z@2|=glz3XYF>z_fIm;7iOi8|-KSagP-CuKfg+=|gg1kUSj+Dm6!o_htD%<7-m8@Bz
zTfIm=#Nxl*r8~DP{La4U&F;yn?^*whO(o()$;I$)%SZp$7W|w0lt(pXvQD$gr9%sg
zUd!xUVEFsvj=v?XpWo})3mw~NF{j#?-SpmSLnmor_2NXI(vy7uTUtNA=jr>nTkS+d
zaCxAu)c4DIVJ5qlUC^%eepnOpsA$EfIijaBGOJD{#aQoJvo-m2#~Hh{ZO_(g%(-8`
z)!y!zf4{Y@`LgeFtLL8Qytr=ad>N6;A6IOiP`F&y;(dw9yCoqn(&S~I&X~xyINDd4
z;YUK>nhp91cD@%E{%zT`qjOuu?VX#C_O02zzy8#0PaEe4FMg&3^D|l&q_OXuC2J_r
z`PO`5ky-v4L-E2@nLOT6D+BkmCFR^*tP>;fA-=xek-;suqP!sEdclI_-^30ryuFqA
z*XM@xm}OIx7$weZNq)AA_h!_oxuz91ebI6@w@&ITzVgq>uxnqyIUiP^YMqu&O{u^o
z8F}+vm*}{DbZ@`>=EJKXLm8FbZE|N-MU>3+-btH&y4(1ErAmFzC6kva8~pUxV>EJ-
zU+pPqJ2Tg@{&<Y0=&OsCV(tsuHn9k;`{%TRS2Njr?U8A_I%X<`<wi-*w)B6tXj;~x
zB85YlnQz`)-MaBa)g!m(6F1~2?me#HXUjjUV%DPtn!dH-@A&2<^%k_4?kbMp_l$P!
z-0Ja2tXp=kiqE87a}SuY9qNBJ=blX8uhe}nx*Y}CSNb-6F%+!NtSR*|{Ti@)G1u9h
zF_jNLxmJ98+HJcaxR3Qk#HYxMnf_PLU0HZ8v?QMIgJST-6ggcsmIrdhe93`3q*XKS
zo%m;L!O+(2y3%#agXxO{x@H-D@maY!+=P>Jlb*zqn}3ug_j`!2zjW16I<r!kUGZ$o
zEQ9K&>+}@$cbRYh#l65xqMpz8*7k$ZM`VIGOt38L_V+sSZf|zCz}$d_ZkF5)7mQn3
zmUb^+apHvOM3=sOw_i#dR_)m_=bL$coL<d5DgIe0Qg0TX+?{!Ac|Lay^FHQhw^oR(
zUnj2I7wRpVa{fw)j#Z@AvN>m6&K#`ztH5XZL}6)(D39HSz??D%J7&ubAL=#hyLb9O
zT%#wwLox611Oeg3qyMHDPI<9#hl0^H(@&2~r|w;FJY1x1n@GTSuf50RqDzz4+2x<y
zIN_(VCP#Ppy?J-uU1xH7ePKnh;k@aJo~IYMoRd0OX5(1>Xx*u$2Ob=`ey_UEW8v)l
zj}nu_`_HEHzIgF`$NEnpvwrx;Mn>M7w9qQ4KIF5~B7?YNeQ)Mm6cOLN`2xe|n;s9&
zu*rs&d{=wnxFPfK_RJ^wnse+=Go<8&dR>?>^+=`M|22J=BKBNe@@l_PrTM+J6|zj)
zO-*8Y6DMC=5a{!?R!=YKT+j1hpXcYlzGhiq!kuv3I`i@Tr3#B2Hpw1ewQ8rSg?!70
zdynH46dF`rXGbP{m~>;Q%BAc>ei`o;9NAS8{yBPG_nsw;)tU<I%64wcxXZ3SSQyTE
hak@nH1-YcDOD8;beShzdO#<J4=1PNg4>Oz?7yyX3*Gm8Z

delta 2437
zcmZ1{@=JJvY`t872uH$#8~y*HJf@ULCzxvn-T(IPzP!4e`nMZ1P3|t6UU8A_ZHAkE
zjmt!SPgV_6r4_AJ<$)H*TbdS5@6c;~qjybS@7LM4N9E1yxAFgcwJZMb^GDNbs)MgT
z_|!i8wf^gZ?=A27<4#$vE91>>Sb6yOpQq2tF2C9T;e%PO^_~6R_3X0mmo0cJGQE24
zwVIu^+u!}XzWV-qyMopHvv;?@4gVj*eCyS_eZQ)*CR#II`?#<6ZMyur_J+Mv+iplz
zx-B~7SAAll@iR6-J+uFR@93>t_y5fH@Sjzma}2|lUvqifEj}S_xA427fF%)LtbLxf
zn%f?0I=WBy_0X6hH}TbxV|()~>lM?khRph+(A1gya-wSax2-EWVrusN+;nmF>#D6g
zckTSgCR>;MX?4HDt=SIkFQkGO>4>Tpdo9h1nowVMApAKypTN&J=i*D;X%`l(^?1r-
zr^GnDyFUK@wl({oeyTQJux_1s?Y@BM+clkEn8Q70ofX;rXpZC@FV)4|J1c@;Oj^}l
zUz$Fz{`7V8@cDVO<8t|yAO7=mTW#L;QuaSNrrB}1_wvi^+haezn{Oa(pwr(`V(}#F
zTiI&OmlquiFR9L}ZTx+zML21PlnRTEVG?U_deX<es$4f`rzVR>=&Ny;1<t;eR+o8M
z;k{4n^)0iX+||$WUw!t+^T$`d^_yze><K^GAI)zP#{YZGaXxmQDSP+wzwe*y&ZJzg
zm(z6l_}|1lX0^GDB1c~AJgTATd{HLo6|dH}3mQ`{+-4LxzWV;m{p;Hg?c<5~ArkS=
z^?=lhkXO$>%|6d+F|)ZOuKQ!77sJt`>4`1sM}Do;__aKM=YHd(2hy%tPrUN<5=Giy
zb<HyL(`5~R^w|B>iQ{>H%MZ!!o0ETRo9H(K%hdFGMY#a)IaO~>TQh&`U3T)-vD5qe
z4CRw;7EBhBxgrt8-w@|?UQwH^ONON)use<U-P+$Z1~MVNB`a^HyiYnAmmJcTW@0j7
z$+ZWC`mG;$<FeYg-UsV`Fn-vZ|F%;#c)IQLSIge()vHYoWEN-Na9plOZI0^Xd}diy
zcJ<!yboR##Cv*CbzMizJC2H<p*6Rx@l+WmWbqy}*379q8{!9Mkjm%O)Js-R`|7u@m
z(YxjPk;`+I^L*@|e3x0GzN_z<$6U@P=D^_NYZ#N3gsisw)sVC*HBGaE*IVJCrcp)S
z1>S^o?>*cH9ZIg$zV8e=#ktk${8D{|C+}SUmUi}>6s|GfThb!BINeymt+l#eXwTf4
zcaDEq*ys3j5uZ-}H)+NLj@mlsO6;%2%r=(JQqdRX7M4&xvnjjys4X{#P`zk+8^f8-
z8DZ9(dcQPW>^z#=Ql~Gxb*CnG`~19L%Xf!dJ*bot^WltHzHiH!sO|U8+0KifG<nMd
zM=!gR+B(1D&c)=p-^~6LeEhVqqMH1>;{nd%)0LQizlqdg)3~|lq+jgpqb%>DgN*(-
z{I1Wx{{PmWZMFYD>iw^{pf1x~Y1Cg{Z~yIJ1N+?hi`j0~EPqz}>CMV(ixdn!@^&h<
zPdhF2ev<QvXU`wJZ3tLeVfrdy%7z&i3^!B+IBIsR_`)M_=+B(x#SEDZ0h@$N)71BD
z%WE?#>HZzn5qb2+wIa(Tt3StO9xRvtE#6$Ap)2+Fi_hN90@gtJMepxjf23nm=FPhL
z_}drtug)xxIgzyMRqgAuteUz@o-{0)d2L3_+eW=*`uAtb@3q%{e{IA62iFQLe}wU7
z8N7Oxbl6L9Zt;Y-8pme|eU#Q~*dN^<$oMad@y?A}jue*r7Jm9}-=h3At-`KMv%ToA
z)$m^;^Ifj#@-&m9rf#Os!it%NbW*IIu0G25@qZY@|AX~KZ9<zor#T8`J`C7d+81*{
z;#WmZTrA@s_S5|>g*u;}-8*x!<m<_fOrJStL=CU1R{!GSeqb*l^ElIY!p3Fq7FC(>
zEtl0@RPMVl{MS6DA3Kgbo$%OFd&<R2U#1+jC@zW2K0ZxwX6>1rv-blS_UG2uotiIS
z9+&5H**1)MzVPf^?RtAljb(=e(-+<kvo5&zGU1Nr$_r=htWJn3^SaHR<;L*gpiE?9
z{DGQTi=2ORrWOk4e%w~9-YpiH|L?~f^T`!$2M&I|xa=MCrsrqA73oE@+Y4QJuXH`<
zUPQ9qqmauIaa)2GSMVN<*zO*w@#S~E{+Gimc;&zGy_Nd*<;p#$8|Ayp>K)?wD~_dl
zX$mzQ^s!D`SH3XZd*^1h{`QZ@o87HvrB1muU(@ZP_^FvI8#4P_l?;!j$r;VMoi3>9
zeeuV^hbGp0tipNNPp(_&Ud-9r(Hs2Rt+%H9LABON`9&taR+4KLEB&8&$ZXjG?(`FP
zBumaz1}&7En_MW8rQxmc@Kt`xtqJu;+pc)!tn8klnRIp8){Qeir|4y^+@@WvBr|=7
zU!0?K_fq$~61j_~WS4xGII{A2oUniJ8`GsL-yf1~NM0kzx52HP>$PI$YK@Izo_CTq
zE}q`v8MIya#<7NP7w=r${Woy`Iq_OEjYkSwJtx?yiS(}T(_Ac<RUWd?a=NyD%p#8S
z`|4dbGMAj1${_1yr!Dt(#jVb&ODj*kIn8L7qBZNx;-d`=caqN~>bxsk%yL%xW<4AG
zfr4!sTRX)56p45R2Di=AEdAD{rs#N$wb^8Ly~^YC&PNJ+J6u~VOCKpLnHeCQw*Jml
z)hDjspM}*kUtv4E(EYbrMfZ$kE-|Cyc^^GHZ|p6v&lOyx%vCUL0k2rqvIz@HK8lD+
z?o^v};$pdVt+HFcc<1GJY-dlmo)3N;H`%Az)}+$h_jk$F|JEO54X(Q_ttj0qQMe{*
zl|uEhWl0xL1_eGzQA^^xcALHMgd)4<($xtc8hevAGk=mi(b)RmJMv5{S9<Ba1H2#g
z_&5y(Bi{H+I@fo~b#W^t$13Z`ncw8Bs<`@K>(Yi@;je7J-B=}E{Pky_4EId?NlhCn
zO5dJ*Tc@qCg|F92{Bfn^q%AyNPu2+L92efA{%+13ZXUmyw|k#=i0t|))~{Ik@kY(H
zhQ7GtdnYfybfo^}tCOFm@mv*LJWE`#^<z+J%JZIOJ7&ynWt-veR?nnv_F{q2ZevIO
zCSU2g>2Ck#G5y%g<M1qODGP6;=bYysuRqr4JsR!1>Yw!F^2f5B+Z8t`X=FSUvdrX_
zIvR5C`6H!gXDY0Ymi&s@@5|t|nW1b?wAsHZP9-jt+l6aZ&5CZm?8x!n=AR@JQ^cm3
ztZe$7v0h4h)!wu`<MUeMU9M-i|M{)s-clQ;GZh&;N>1685Y8)CHC3Rtb0hm(#jr>&
X%eXImXJ0cG|B#<1Is4uZM+OD}DtE7>

diff --git a/examples/vacid_0_sparse_array.mlw b/examples/vacid_0_sparse_array.mlw
index 8255d26199..534a818e53 100644
--- a/examples/vacid_0_sparse_array.mlw
+++ b/examples/vacid_0_sparse_array.mlw
@@ -36,6 +36,12 @@ back   +-+-+-+-------------------+
     forall i : int.
       0 <= i < card ->
       0 <= back[i] < A.length values /\ index[back[i]] = i
+  } by {
+    values = A.make 0 (any 'a);
+    index  = A.make 0 0;
+    back   = A.make 0 0;
+    card   = 0;
+    def    = any 'a
   }
 
   predicate is_elt (a: sparse_array 'a) (i: int) =
diff --git a/examples/vacid_0_sparse_array/why3session.xml b/examples/vacid_0_sparse_array/why3session.xml
index f1e56e2cc8..1dc788d645 100644
--- a/examples/vacid_0_sparse_array/why3session.xml
+++ b/examples/vacid_0_sparse_array/why3session.xml
@@ -5,7 +5,10 @@
 <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../vacid_0_sparse_array.mlw" expanded="true">
-<theory name="SparseArray" sum="bac3050c05ed738e09d82910b1b02112" expanded="true">
+<theory name="SparseArray" sum="e8b16cb41f767bffb87f7ca60d376375" expanded="true">
+ <goal name="VC sparse_array" expl="VC for sparse_array">
+ <proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
+ </goal>
  <goal name="VC create" expl="VC for create">
  <proof prover="2"><result status="valid" time="0.00" steps="25"/></proof>
  </goal>
diff --git a/examples/vacid_0_sparse_array/why3shapes.gz b/examples/vacid_0_sparse_array/why3shapes.gz
index a5791d332cfc9ffe7a52105d30dfb6ebfef4d6f2..458cfe3fa757acf14a6ba73d6c0abbd4a8cc59e7 100644
GIT binary patch
literal 1578
zcmb2|=3oGW|4$>mvt`@`_MKmUV~+EJ)xUVJ9b{qQKD6_!>WmBi)xy=P@B4cHybs>|
z`Nh1s6H}b@wzUcvhhDw=b=`XRNEgM*X+0Ztmbex0Se%cNo?x_eLw5cBr@t@1`}4r>
z`IqU|bMJ(gTRc1b_}#Hu8=G(Z_4{%cR;8`YIQly9#nnj<?Up>={jT<O`aj<U?}>kp
zWV$A7jnK}EKkwfE`@ok2VLEoFr}%QcUtGQ9d8=6TD%NWSb1S*nTD}~N%0BQjr^4;o
z)TwbFPdY!G5;J|>)(KnF3{#aH6j{o<*7D@s-}~;Hez#~>`9t|h2c0ZslB-mN^q1(r
zJN&#v?UqdMY_S_YdM?&$^;C@I0yU~a76)8ekokBA7w4kny}=I3dsiP=^DM)_Gfj=Z
z^yQtMhkvgBvT(7(YX8?ZQhaNLl0tfxM4KLOow9qyrZarOKMYul@8m18zgg#H5&eGk
zvK2Rva+R8|+*t3}T9qFA_D;dMt$|a#rd7`u@e($$nCw*GaaB!Ce6M%x(+}QDsvduD
z@496@H}w6{$mEnv$EVM3Z>`<@;L@4etyzaPuU`s1XQvyw$#tFI-i37rR^Lj69aoAZ
zxhz|nYNvHDR7kQ?U|M$T?nN?hcH7@MDSKblz2);16IF%!<rif4<rH=wdVS6?<#_JO
z!-*$#w%<Q-J@9WR+xCd8&sW*L?{vuNIG<(S#(F%Y<CJ%YmGs-d);E)kl%mfcde?3?
zKP+#G?7C-8$*n$22O^FsZIIZTt`$5tRer6v(ffI4=FdOo>gGB@D^>PjakoaurxneY
z!_*6!bh+N8>zW_ja^YTc*NaUbW);fq{HWk)wVW}%V#=<auKl^Uw<$d5<16~V>`X#r
z=~Jb3QFp&z(YAUu?Q^C4xz)86_iwa6`Q6(k;1{-7uXp<47pGY#^2)8q%xK@Clkv=`
zSu035gyTR^h)&yqEy8-6c+{#jg)Yx1pMLqp`*%$W<^TSDHk^0;@?o9j$M4E){GWeG
zq<H;>gJ)NjXoMWzvNxBd$-_%xzJ&xk!@Lg@()>CdUJ6`V_xsm`6Z`bvl@uJ$o4Z^0
z!!Op~It)7}Zeh-6Tc2bd&c1Thz6|q-Y18gBoMshyJWI3dhLn-;cPZn`ovpVcW;q_S
z(v4s^JLQ9sr7LUmLFtr}Z{++m@5n!1XnjXMz9mMr@#O=<IorCp<sV00F5t-UZBkrh
z+8OJV<z4;q_O+vXE^c36S8aXa%%(}lrsnLmjn+PRZI{^zmjfA-%M{jJdSb9ZbLkxJ
z8A{wW&(A$CS#{Sq%l>!9{jX2$x1|0~w&H9`o#ZAEtHg1wVzElrDoc+Tm6wx$U-JvP
zdX4Gud9&K>=W<V2UgAvFm^-H<W2<o-i~OF@4wt%vt_#xTb#Lpw$e#KpYH3|XuUcpq
zZ}`Dm9(%Xlj;T(+mdthN)>4c6;o9}F`md|+TJ7t7aFR=J=F}3+vq4=sE*tt5F1fix
zwR&gz=UtB%Elu>=A8q^l(CqyR2ZU{ZD}`2>y=^<q@xj#Zb*aSsg144@t~rm5+1FH?
z@xGsVTOrovCDW@?fs2=Nr>M#7c;dpaScq$T^$z>;>%P@)Qdw-`wnhh~W<C%z3JgEN
zl9m$0n}1F%B}kC7mFL8gWxe4aSaWyCCWr26X%`S%-F7@a`bdCrPWPU$#ja9&eNS9z
zwD3QrzIe-{nVN@;jk4D7Nu3zV@PXZ6`-@wP_UwJdcEWsDW2Vq_Gp@-~LT(j0xpze$
z+xxW3K&W&{y6u-7roR^ZvR@o(U}<Mj>G>ki;&MEN$BAR^%WYqB7XIBn`^dku<%Vaq
z1TH+u*}=@}8F0JA<fcM%s+;7wiUq4*P4U`truN^3Qr-sDb^K8$U-15%I`fD`WAXXg
zYnA^#Ni4`d@zCa&hR{O}cga^A|D&fws&N=L%}$+|GFfrfmOD2ONK{SVJM|vNyS*&4
zHcx(2U2e7P^G_{?ghNNS#2w%Hc^dzj(<`lO{_O2jeDFE?fq711Q%t_%{0mNY3tQvz
z4G*@f33XgeSnPdJ(B<+u@Abw%wJO%_@Si-r#;Wam`@{6pQg=3_y%OCY;CPWY;_BXo
z_5Vwb?w=hJcGaF&t9|8H!SczOUn4g?U1YZ!Bs2fqqIC-9Hqo;$|Ka}o(tSgMBm)Bg
D%_<ez

literal 1501
zcmb2|=3oGW|4$>lvt`@`_MKmUV~+EJ)xUTzIkK>DAKH0Vb;bq%YT-)N_kF#8-Un~~
z{Nmo+i78Hc(~c^oty;Z$^}eca1#>I8*jm0EjLJUnGpEAs+0?0VAANuSR<oBedpIFx
z`klP_<^Hp?%jbWS-_^f1=jK_TZcSlEF2x<rIjIS^-z~en?_8M1z1I2;cJ9>e{VzK`
z_DtBf>$m<(4->=7Q3=L71>SDiJ>g7+%fc6dy-tD6%X%McsdV&xUC`iG72X(m_F}@M
zGd>)pFK_I;`*D5A{jF<4=cl{czn%B1-Tpp*`=%}f4YxaMXYuV*dg{08OhrsA`?Xn{
z{M`6H^nW_{qv5XT&$Vlxt~#0hEvJ3g>?=3+EppP044))@Zl_t->ztk6Jr|lVHXCcQ
zwA*AGI(|_s6@8%Y|MggYx#(8*xuNe_*IeAZWnt6LvdsHuD)OFfyS0_+lxn%?=JUl<
zGbVNiua7oltiJ3Lpw%idF*9>!zgNLj7dN?<r%?}=X|UgZ$6sFXoByQXLkm{l!V~v3
zOLni%UhSF~5iXJEEyov~w(qUip1xQ5N;{5DnjNmaTHi9MwKi<Gp^n8er;s?OD>pOx
zwNj=}5xiL?W|n`e=GM+hWfjp`_Y`()bW&qX&`B1I=(%S+RrCC&{%fi;&Cee@@6S9j
zP;iM?r2B_EN?cQIUOm`ym2*x)I_LMz%VsA;WxRKEEs3l+YtetFVuHfl%MHPI?Uv=~
zT}-~YP4~pkrsg~Qv~458LU(Rh9roSyYg6B@r!~_KSE{yu7PUNbpIghvBC>avNF1N?
zv~(9Ug@DT!`06Yd&kW{Y<>4Ek$lx8gQG)5R-;NVTGu|xq@JYTm$8YifDHZJBb05p^
zd-J&PrtO)^?>lDOe*0fKE9u?Ql7hV+vPD-f<mO8^DoheOrp|Yav0-_ohw*Zk1qB?L
zmustiQtpSB-`H8Zz2~l2#owk{k%kz~TZy?wLPx6B@Wq7IO*FCa*WG#IXI%SB&gtEY
zHi&v&eWm{0ML)IEPiJ-SQn{2hmz!8G_;Bh^4xVBlvBz=RnP(p-96D_GZr9zz|E^A4
z&0-*Hv+HtL-NVK9*;0IbYdsArwy15K?47HrUwhMPrg>8J*W14v)6N-Z-Z?q#(aj*v
zZCAEBsxi6E-ol(XRqa5-t|>)&30*oLdadOyFKkP{Qg<xl_Scv8Q&NAMIW{HCTq5Q&
zokJ>nPoR+LQyCS#NncLZ=ButOdY#iYKlfMS!CVfRmo0`Oets@nZb|Al@!!*OQQFTW
z_(F2==OXT3L8`k$R_4bo_MDn@ICO(qkp5e<=`YSy`S?XRb$zbgdgyggbo}dS|8iOU
z!wOEWS>l~JEht5~sgy_ctD5f3*QT?ti;C--2LD=n_08p5OL*JUv%Yn%zLGPk?YZ28
z)0S(mC)ONNEt287y(#VTt3_$SpXY^3FX`5Zb=b?N6t$~2sGWKG9FBw#r-x?!{KwyI
z$~Zr{ZB~1CozcN6qk~&dy2SdZ8ThM(etwoS%STJeSMhL4(B)&=KO}Q^$R<zSW5TaE
z=dF}neXgMM-h}8UTcvb^UgtV3<2q6qWGA^)^t{hS8|B5{PDP7FnlkKTEbd;Xd+K&~
zRzuBFsTpd8nTriPJ(tQZf9X+pddK#di#;x)FI`*WcouALj&&AiTT<xZaL9w-(WAuY
zm_o~inR(v&YPafld*<B#D{yy>6w|CZyyXiNIJIW?SxKjCIHPe`lD{N$u2bi>o%-Kn
zuQNnMeRb59+^ZNf)3fJd!MmO3t<J~GF_-W%o=fggx+wEd!%6n+f3ehQoK8It(&AL^
zrF5w2mYW&0-Am11YTi_>-}vjzk>3|(zrC#3Q@}8zz-aCD!gYHZ*OuRX`1t)&e#UsQ
z#`}tgSaymi&cEnnx41Q~YsRs5wMzo454ufnS}f>mt-tqNOX!D~!ue`bYHqdn?|ztn
zRw`y=+A7ig0ZtcrBd%^;SpUCfW1acRHK)=)Nf~Uld6Z|g*3Nrd%$4-7@8|1ZTfTXP
W)(O#+?BZGVjJ$6jOW8><FaQ9Mao3mt

diff --git a/examples/verifythis_2015_dancing_links.mlw b/examples/verifythis_2015_dancing_links.mlw
index 3dbf842f29..67f34c98cb 100644
--- a/examples/verifythis_2015_dancing_links.mlw
+++ b/examples/verifythis_2015_dancing_links.mlw
@@ -61,6 +61,7 @@ module DancingLinks
       represented by array indices *)
   type dll = { prev: array int; next: array int; ghost n: int }
     invariant { length prev = length next = n }
+    by { prev = make 0 0; next = make 0 0; n = 0 }
 
   (** node [i] is a valid node i.e. it has consistent neighbors *)
   predicate valid_in (l: dll) (i: int) =
diff --git a/examples/verifythis_2015_dancing_links/why3session.xml b/examples/verifythis_2015_dancing_links/why3session.xml
index a5cddcee5b..8d7d3ab096 100644
--- a/examples/verifythis_2015_dancing_links/why3session.xml
+++ b/examples/verifythis_2015_dancing_links/why3session.xml
@@ -4,7 +4,10 @@
 <why3session shape_version="4">
 <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../verifythis_2015_dancing_links.mlw" expanded="true">
-<theory name="DancingLinks" sum="4d6d9e4dce7f831bfe2d9977d64bab0d" expanded="true">
+<theory name="DancingLinks" sum="6da03c19828ccafc3450812ec12bdd7d" expanded="true">
+ <goal name="VC dll" expl="VC for dll" expanded="true">
+ <proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
+ </goal>
  <goal name="VC remove" expl="VC for remove" expanded="true">
  <proof prover="2"><result status="valid" time="3.04" steps="1747"/></proof>
  <transf name="split_goal_wp" expanded="true">
diff --git a/examples/verifythis_2015_dancing_links/why3shapes.gz b/examples/verifythis_2015_dancing_links/why3shapes.gz
index 4027c86b7a5e2f5be7f43bf5ed6330054869300b..807f5cc53ccd61a0cfcefd2ba3547355e9605746 100644
GIT binary patch
literal 794
zcmb2|=3oGW|4*lRXUkX$9Dn~;^Ov01E5)fQ1x#uN2`6^yD@tr#a?fPuml-p+74G}H
z>g~(xXJ%AP_dT$Cx?}9pmA_txFJ%uFNOV;am^*Dkj@J>-5+?7Y9c%2Soz06s_V(KL
z*vod)-v2c#t^XFU%~4RBb@*gu@v|tu|M%?pn$O2;t<mtAyuPi!@Y>bi45GPakH5G7
zkv;eL(9<0OAC2_pA9;Ft2dgxDio=xEhE9v6uN})spV%lc%VN@v<?na5Ke>JQ?Kayl
zqN}{(f3xq;ef;*_zn9UzQraf}^5)BJ`dYQE^Zljd{o69{>+%YloLpDDdgkBFn_ut$
zwc#~iXjqBKzSS4lWNfCMJ1oh5%djaf(Q)@o#^t&75?A^H*8lqvByrtiu11v;yVw*)
zf!xKujUw)^Pi^adY50Fy-Tv?Pr>e^DA3Z!Jyf-s-YFKU6F%ywDCq$QR?J2pfCtiB6
zr~m&<-7h?4i6^tyCj`3)wOh5TB>2r*b9hC=XRV^8#S`OK-<q?k?%en8tLYaV9`vkV
z+uOT&D+})u-K@8~PJe~J2Cuy9wO2N@KI)Cs=ig$j_p}6?Gjxu)i8N0>uys@AaaP&5
zXrUvezJ9l-PkZ}2r&#jjo|MS9;SyJLk33rWPg7sk-FTU}T1eh!{y=fw=;p4qr*#u1
zbDL?T#x_4G`m9w|dSB^pyQ1Od<!wikC%sTDJhk?Tsq_^QpFcOhIn*tjI$^rkgnLHY
zl$dsgIG=F$Sj8FgHn=E*hm(1=$5MNlOZ)Q6@8<9I?=zEGwIQKbJJ0eet6Ndrwuk%9
z=A0|keU=xelQnUYcy3aHx)$5fnf=_oo=LNg?YK4VZ~yKozh4}DfBVdX_xG=w=g-My
z>@t*h?%JBSB~0W(s+p;KyMj;1y|;X|ap5`htzO1giSAX*Y2B<h-{$8_k6W(Otv%g4
zZ*A@qDXKSBZ<)6K#O(jv>zhKHPNtWLOj;0==H_?RG-9g1#?x6JSJsx_zkkiHX13wS
zrRp4?w5H1>ev~>Ryk@B{?}i_Hx_*6fuK70q(FO5>1HW=4xnAilndNr6+Hut*{j2BC
K@l5AsU;qHpY>w0b

literal 721
zcmb2|=3oGW|4*lRXG<Fj9Dn~?^III3RBs&fNktK!#yQ`EoG!e&s8f3F;BLcn+uvJk
z{Ql6wL^oIA?a>qUnWpuB)4n)(J4GdmTorJ=Cb@O%ESUup6pD0K>!-%8JzcshI(Jh3
zuGy)VzlyH#ivQ6YZ}u_m>xVD#vA>p`J-f|j{efS<OK)wcGR!)*J@fW?)3>)*KA67p
z@3s4%BHmT4ytT3ZP0sIV`LNvZjf?mGSji-wa6LFPPp)Qe;ctV(2ET7s3ars*`)sHC
zJMa0obvNI&tWTf6p4<E86;C()#unjIT!~w{^;lOLSZU2RTc-PeTHW4n{i%DaGLp@Y
zgtl);6AO#AO%|HY9B#Pgsl)b6Z8=M$!+*^eE6qRXClXh!D&{(+&EfNuAO$sDS;r8j
zO3^u)exIUaZzo?r|MB0ZYBSv>3a_)DC#i+cUeJ1lZ_76^m%qZ_omXW(yC)kH&&#=Q
z-J9RKTzi6#MKHW}IpelaL3l%0UwO=hhif$%XFPwhqvq+Bn)#+lDvu|f&Dq~IcXwx`
z#W(vSQ-5FUcsZ3(RJTsJbmGOxfEOL!2UNNAG@fcStLVk4-jCU?@ITR`<3+05W5t;-
zd=DL2`ouKqg3*m1o8L12@X}=To7?c`#EmWum8DTEc1}UMt*dIiSgv_BGlfoB`hM4z
zce6u(uls&7t~pjrZB62_Ugx<9DRIkk%kLY_p1wmZS$w_PR*#d?xycSjT5PRn+MTwY
zyfH`j>bf`b?}e{lJhoms?ZfNxuTR<2qd8g+9G~E{cJnnaHifj{WEBCnr8@7!W6!_t
zIvcF|cVYNN_CsM4l<g{iywostedKlNqRZPrcgY?5J_#;-sr~6w{lid?sRuqt%J!N#
z3K~yd@+!*WsQQ#eH5FO+?Z23B<-hOlQ}K$E$)Y>;+lB(ZXPnnUf~_Nd7<K>p;#~8_
j{@6nQ2Lhirr%n&B63oi*ea{*!YR_P|r*&5^4+8@L*0yBW

diff --git a/examples/verifythis_2017_tree_buffer.mlw b/examples/verifythis_2017_tree_buffer.mlw
index 34a1cf7f2f..0efadb17c7 100644
--- a/examples/verifythis_2017_tree_buffer.mlw
+++ b/examples/verifythis_2017_tree_buffer.mlw
@@ -63,6 +63,8 @@ module Caterpillar
     b.h = ch /\
     xs_len = length xs < ch /\
     forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
+  } by {
+    ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
   }
 
   (* for the three operations, the postcondition uses the default
@@ -126,6 +128,8 @@ module RealTime
     b.h = ch /\
     xs_len = length xs < ch /\
     forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
+  } by {
+    ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
   }
 
   (* garbage collection *)
diff --git a/examples/verifythis_2017_tree_buffer/why3session.xml b/examples/verifythis_2017_tree_buffer/why3session.xml
index 71f8aeffd6..4be4499250 100644
--- a/examples/verifythis_2017_tree_buffer/why3session.xml
+++ b/examples/verifythis_2017_tree_buffer/why3session.xml
@@ -47,7 +47,10 @@
  </transf>
  </goal>
 </theory>
-<theory name="Caterpillar" sum="9e3756c93ccea25c9afdad138a21988a">
+<theory name="Caterpillar" sum="1d67f8a5b1422e0c9043537b5ab5d545" expanded="true">
+ <goal name="VC cat" expl="VC for cat">
+ <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+ </goal>
  <goal name="VC cat_empty" expl="VC for cat_empty">
  <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
  </goal>
@@ -102,7 +105,10 @@
  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
 </theory>
-<theory name="RealTime" sum="229eeef95a917cea47a0cb02824e9fca" expanded="true">
+<theory name="RealTime" sum="b99b5cbae9b2f754fab20d968a6639f3" expanded="true">
+ <goal name="VC rt" expl="VC for rt">
+ <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+ </goal>
  <goal name="VC de_allocate" expl="VC for de_allocate">
  <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
  </goal>
diff --git a/examples/verifythis_2017_tree_buffer/why3shapes.gz b/examples/verifythis_2017_tree_buffer/why3shapes.gz
index b1cbdb393ca796de7e3cae589b74d04c49dfe41b..3dab0eb383d0488c0137d3355c2e34c631ccbf9d 100644
GIT binary patch
literal 1776
zcmb2|=3oGW|4$=*^QA3?_P!4PVJFcLsw3u^kj|hS!OYh4X6<^%i8^ULrEk`(z3Kb!
zZ<zL^UD4B$j{8kue5TZpWA^&vRrdI;3zj{L)tI@#>|E&TT~nN%&rw>Um40~k=DPCw
zZPV&sSBZ+&@^74w(DSI+<;9AfY5Z@p?ybMZFMoahb?p^1TQ>_7T$;1=Huuif8%aDu
z8T(_RqSr5Z5;xha`);?{`K97(juuRq&QiDi$KG|h8`+-E)!G(yWpP38ImdUbTBRi>
z?SJ37+1Ci{-1qkS{Bw1a3$s4leyG2nC$B-dxZ-D;ZvOiGY3o}vIp4-bpLuw-?91y1
z+J9cZE&H;&cg~)jyK8^kH`wv{=(YbpayyC^Z-0Nio~LHt{55$U&+~uD9G<{-FMpFk
z$<Gt#PMMx<dNG@6*|I3r>C+aipBQ}cNc#V&zq5D7&Np5AU5mdeLHpLhdD}{N#{WOM
zCQv|6Z~5e(cTe7Vl=3g>Y4el|!7nXWY>#j#SvP5NoXar@%ik62zrNcRyMF!qyyd)=
z+Y=*lPS`UkE$H9Lv4An<9M6<3Q?BXGi+#?PF8^NcTDwHNc!G^C=kDub#r|wJ68=?P
zdl?}*YpLLdh<!`1?Jl~)F=?0gk(X1K&)%4~yhco^OINedJHq73tk~1MyFyu%v|SDN
z2wiMi{aHEi<N5T3J^^d=Cb~NC-#dP#*P!*@7RH|)Ppv<GTU1f;b7jo=5QAMwTlcWU
z&za)pn0!XVFZPb;l`IJ{jzTBq*%kNB)m23tQS^IYruH$({!U_(WF7ajyKn0Jc*<H=
zUpz52CvOJVv)+iLG#-|{liNi$G#Bqo-SD?&_QSgEmFfGVC10G@6FztL$(={fCpykK
zHec?I(N5V6G5g1knIA6i_?MVmUbt^bW|?<Ia=LZ;`$IiT3LZ@VFhj*&cjm+=&s7da
zY%o{pwO=h3>9Kdm1nFfmS&ZsuPISil-+9h+)754%)6rvMo<|+x<mbl+v_9syNy?U2
z6fFzxcHNdBygJYMc$0@r{e#G5{dpUm3m)jp%)EJi%^u~aS>OFOc$`0Hn!Yl2&zHC@
z>MM?~Tcn&f*LjAeggD=_<+48hmJ;l{ZV7BI{rqI<;pX=%ewS|EbLgno)!s>~g7gA{
z&TuZ?RF-4O?jGXrdieF4G6D9$sluX*9@&WHc?sEQ%rde}EG_#dK07Z=Z0f?>o`Gjp
zu2p`T({$pMS!es>WzXML?99C0HFZ(aqV5Ri?|MdC-tF<<J5$2?=-2O^Ys3%p1)K@L
znsmf5RAlX%OE*m_0?*BuH=A$%{%AQFO$C3|V?7&xzPxW&TjQT{ww=Q|->79tsPDBS
zU)Ee}KN2@@s-nI*|C2Sc*-NK%Wd&xtu3Q$-!f1T7%E)oQ)5X`0f{RVV`fiGzz4jtC
z+(+rw)TUWFTm1`)bUNeu4o*qjcskay#7kuI*9jpt#Yt~{8p@O=#>>uF&;E{~=vV-&
zQP^u0hpN=)6IL$`^;q6@pY7p^2XedaNS3U;-0aU^^nLO6<tbj`&g<SRT$J2@uq$fg
z8;@(>#cdSJ|C_yX40H7<Ny`=$b#WG2e~s<Ogt<%eGZc#1_gr6EBPY1)B=h17IYvuK
zak0r0wcU2Fw^CET*Ze$d(~=2SE`$VJ68ZMMUN=_G{iE-(rpzLi$>P^8L|*4<++x12
z`s&RubMM@_BWb=X&QkcJn%{AbKB0|n7p^rK&&`_WefDkKuZsHcuMZ#It^aq${_8IP
z@>%!R$nP_m^Zc~s4ZB@4RNrj*VQKx~+r^&`ldLvb<jC6^ZI7%e-1+C)CR2kWD{DXB
z*0(*pfw^wu{miM6J1buuIkr+?Rgt-W{u`fb+)93mAHU~Rri4y(esLn@QPAv$&3$(n
zvx75Mir6Q=xNR(?^FK)YVhGdIgujJP#A*t{a%w$hrO%GuIdl5H5})>)U;Y@RX`fws
ze%gPN+7Gur%wLw@D*f-W0RPYP!vAyn?w`B4yY5*1yhVA3>+8<gpJz6<`4wXM>3zG!
ze)VwHYOhNRX5L{_GFUr7VsG*Wxdqy_u1?D=Uu~Ezt(@0pCA+{c-rd&qER(743iHI`
zM_uvDUVhn`7A}75`o4@V-#mLw4xdvqX1sRUJB96N)#4em*$=jb?#$pk&GAcH;hW#$
zpN7td61L7*yS!)_`${$cwbz6@()avVS+w?S%Pr9vT_=xfaJ^W4W9^y8_8c`L-)vgy
z_;Q}}6!QyCU6Y;~zgypqxu=A^;qiv}>Gt-|7sPs-2A&Tr{Nt^;rR#;z*R*>pBX4;Y
zR&JVf$x)TJU;E`j-?BB6{>hk4dMRr-H&&BnTb;3W##-~~6F7u-JrDDpRe5*+o-Did
z*WS;p)VaLg?D+p}c`uVhHG}+ihITXXT~cY8)O74ftU~Lbw}u~U^RCNRz4*_(n_YKu
IyDS3(0KayB2mk;8

literal 1693
zcmb2|=3oGW|4$=*^JOgg_I_Xgq1K?mBXA1K8J+}|<O2>9_FgqzprU1XZKHA7`Mgi>
zr(b>fZdF$K@xHkV+-HtDtc<+$_;I`3>44zRdQ*HNq@S+}jrCes>?asBb@Rikk^A>r
zN1xtby0@!qUwedyf!jw*rIIT#o7u}u->?08`1sf7U%9f<9_p~nF-d><%_&cDn?y6q
zt=Zn$ucuDAlO2?~vHIe(onM-^O7MM}bl`o@{g=0TOfBArY`nTit~I-auSh>&<>JMb
zZ?<3m^|1NGRp0%;O1|yx@ov6v_wUo`2W%Fb+NQ6+_UYNHs-ICad@{b@O5%;rpI;|i
z(^|jxrrqB}f4{i9_wM{Jm$>sY>Gl0O`9(3W&+h*EyYc+@?yI~X|Afv@mbi4_x33s`
zter*r(^+YbUwj#ZgV#>-_P%)i#LA3EoByA<JN3?*^Rup5Pp!7K(4LjtKfiS6_Wwm|
z0tNK+)X)DpXT1HxnfNs|6NIX?Y}vm~<L)>YT6C%V#0=$h`S)Ay-P^MI>(#esw<x|h
z<LT!8>F&Vt#Za8lq~XlW#!1sI?RvWT^_>TA9>4wjOW^Top&s?g8>(|Re#>a$6<e=f
zd3@D{H9ZYSU+HeWH+8Ywge$R1e)?bXj_s=asp29M9rS40hKv=ayQfK)yykGZ)|FJD
zxQI3Ux%;L^=hYYb1gz1YnCifP@A#EogVuXn7=Ly=wf^{RO-)5-_{Jk=Bsi+n`85;R
zpBJ5G5UsgwdPVE?_Sx_D9gk$2boSJg^4Uidos{Rht6139@7lhs#`uB`-?lWfx~g^W
z-`<R!qt7|BG}`__-r0MtGiN_Muz$n-r`u&2>x>M$|Gp}@^_%h7vGkq4pPpakDi)-#
z_oPj;J?a3baZ%EB;qR8tWed-)aM+mM?O`|}{P=b8kcU6m<u<fhU)O#!P0THAL+8%h
z7d9#g9k>6mWO0AqM&|+neVLgz*RR>5{50#YwMFU8ozK>|bWOk4{f*^ogtxuWHOrRB
zhC;!FDw_jeA{q)8T$fJTmN;)w$%`L-yW-8CiRy)|%A2A#wWx7YlApxXt;we?Ef!U2
zNyn9Cu@?%2S_Ud=olAbWOyywnqPri|{pSAs|7P**t>URKo@sWmZY^Ch$2TJ4zw*a|
zKQAgR=GAY>J{lEh_|a+2!fJ8JsPcQu@A+Jr^XS*_lxv$4*)_ygXIVa4pw$%?_A)1G
zn?|~izi#{a`)m37OeP%XN<Mbu&TsSn-S0bnj&yJMTsC*|mQ^R)8s}a8QuF4ir|73Y
zj~nOony#G^6sViMR`aSzmqEg^2!F8`;Tlzz8cACij~eb?bdzn_n=Vh?-9Z79r+(w~
z>l3~B*>J`ot+Jik?S7p}n<9I<^8IpjI4<~!eCihd{PcjV!#Rmn4#%>(WR`@N@$HO?
zY%N*!GgqLG=iS27YaORs{r&JVF0cN}w<$h`NhhY-hLpT9j0n~alRf$Dd6Rm|V|zE-
z6RSEp&*dmjZ|eQ-xo6g#Z;IC1_b)g+W2{*II+cNE;cTT3nJgbG{}@Y&O`f>gVpYVZ
zw?222ZrJ7uxAhhZcvL^$H9g<={;98D*UBz>J=NGWM=Rf_RYNeFC0Ex%xW>&fEARWI
z<GXLK`u;ut|F7u(*H+ub@>T8K_uq(duKx9e-<OZ-d{%$F{7u8{`RDk1Uv?DU`1j?(
zj^2+)pBDYNFK2KhbKZyB{``kGFxPFopE)&hXXUFS$5!gADl+%qpWq{ZJE7lt*1LZT
zH#e`*D&mlx>9aIbxWLTm)|0ho(>{cB%{Tn=b|r7Cj->aN*VBqlXiSX$a4_=vC&kQp
zxp}45?-gIpSg`TwPUEt$S=k-B|1*CvZGLF)E5F|C&vHe%PxICP-DKJyySe;t&wrcL
zyKVpfOsJoyo>uYUZO)VX{DpN7*KmECvc%E&E|*Kf^t_}meFu+}g#YRi^De%UxZN!6
z4o|6-!`yv+Ri|dLX3Yx7zx3=#>`tA_FMl6gr{A-_cIO=Pt$$yf&6;%}BvAd;QWFic
zlp}X+ILy|Za`lc#yYQbm>AgvmjIj#OweFj3!s&;)vOZnOvTdw5_S;|S)-%%;v5hNd
zyz5%ju&*mN-=^-;v&9>pYknzCuuh**-LWF&u>9{^wI3xDmRK{$wEx}o>!)R3neNpq
zhVDl{*2^pmb(y}xyxZ^WCBIc$CeNM1XO&rT!;?R6Q}Wy|&o@l;dEdc#%}a3uZ{AJE
z?7cf%TxMLb-I{$#=heTTv7a;d)}24&y!Ut2<A2+GWtYil2Kns_J<Y&(Nu^~{)3GD5
b3ax+MT7Im}yDtCg%YTN7uB1s4G7Jm=LPdNS

diff --git a/examples/verifythis_fm2012_LRS.mlw b/examples/verifythis_fm2012_LRS.mlw
index 98708d7535..37be149f4b 100644
--- a/examples/verifythis_fm2012_LRS.mlw
+++ b/examples/verifythis_fm2012_LRS.mlw
@@ -342,6 +342,7 @@ type suffixArray = {
 invariant { values.length = suffixes.length /\
   permutation suffixes.elts suffixes.length /\
   SuffixSort.sorted values suffixes }
+by { values = make 0 0; suffixes = make 0 0 }
 
 let select (s:suffixArray) (i:int) : int
   requires { 0 <= i < s.values.length }
diff --git a/examples/verifythis_fm2012_LRS/why3session.xml b/examples/verifythis_fm2012_LRS/why3session.xml
index 6722acc838..2e23fdedf7 100644
--- a/examples/verifythis_fm2012_LRS/why3session.xml
+++ b/examples/verifythis_fm2012_LRS/why3session.xml
@@ -237,9 +237,8 @@
   </goal>
   <goal name="VC sort.14" expl="index in array bounds">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="11"><result status="valid" time="0.42"/></proof>
-  <proof prover="12"><result status="valid" time="0.01" steps="17"/></proof>
-  <proof prover="13"><result status="valid" time="0.00"/></proof>
+  <proof prover="12"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="13"><result status="valid" time="0.03"/></proof>
   <proof prover="14"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC sort.15" expl="index in array bounds">
@@ -250,8 +249,9 @@
   </goal>
   <goal name="VC sort.16" expl="index in array bounds">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="12"><result status="valid" time="0.00" steps="17"/></proof>
-  <proof prover="13"><result status="valid" time="0.03"/></proof>
+  <proof prover="11"><result status="valid" time="0.42"/></proof>
+  <proof prover="12"><result status="valid" time="0.01" steps="17"/></proof>
+  <proof prover="13"><result status="valid" time="0.00"/></proof>
   <proof prover="14"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC sort.17" expl="index in array bounds">
@@ -351,7 +351,10 @@
  <proof prover="2"><result status="valid" time="0.08"/></proof>
  </goal>
 </theory>
-<theory name="SuffixArray" sum="c7f7522f873a9c6b0d19391ef7745123">
+<theory name="SuffixArray" sum="a43186b5d7cd87edd5fb3f19595e1847">
+ <goal name="VC suffixArray" expl="VC for suffixArray">
+ <proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
  <goal name="VC select" expl="VC for select">
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="11"><result status="valid" time="0.01"/></proof>
diff --git a/examples/verifythis_fm2012_LRS/why3shapes.gz b/examples/verifythis_fm2012_LRS/why3shapes.gz
index 2703716727205463f1069d96abb96a099f033bdc..8bc1f0c0f27fbc684c74e2c8a178f6e8f53ce3ca 100644
GIT binary patch
delta 4752
zcmeyRdP0pyzMF#q4F123oycQeuX{Lf^X{8Z5;wjI*?3~dqOFUil2*2eu38<Ksui#&
zneE7G`Jc}oE-(51dVRTk{jazCuFSUImbH3&TfW_?_u>C<I9-}8&maE&$MxCvxAg!2
zUB6ap{)OlW9rNfP4+}ol#-G^!^zr%r{W({E#_lco9vc+BLvD`wx{AdNYfs;EiCyDA
zv0n4oq%FK3SABi*?cL+^PahVpbdSDavwXAt8k@_r61)$-3cVV-x}&W&^{Cqh-B#w+
zRa^h|udXVuFP&YtyK<Fj*<0&>BGcY)+wk@7`)%&a^zX~GXV(0YkDmSIYs8x$``_75
zJ?k4@aCSR?>aKk^#by3&uKv@xaeM902SqGrUtHYi=~rLqcwwry(Y^`#8)NR?yZg7S
z^z+B^efuBw_kX&5_A!@$XRSnPqVcx~w(LNMGbLNEp6-9~x>49TO8HSTQ~Q!doMw?_
zT@j-GaknO)mjCo#^#1+N|6`8s_Lu*Bc%x8b_Qs^|3x(eoid4<qu2jQ)XrF$Z7<2XC
zPj|NmCVpA7xoGK(IrUS{2k@rO4yfa@y;!?HX5;@0<uA7;Jna5>(qSzdN0Tw%q9V%^
zJmz9T2jYVIi)MN6(ziJ`MSS+G;Ggk!=D!sq<fdJ|bTC@a^mas(|BI%wX)z&doC;PL
z?!0_cr}<mJyZYzHXYcM`{pxL~(?;<NuZuZl1)77^7(<Uwh*AA!R*_m<&wKFoqjhz=
zt1EoU<v*VloZ20hxM}NpuC{LB&^OD@xm6lo4@+q;I?3g-BI#>n=fe{B-IAw|e>t6O
z-hNEdZg#}V*$+MS?H9QhJ}UbC<3j15-|zoz)t?kO@6MMS8)rS%FR%@p;TFcUx&OdP
z_XmHJ)lQzj>3;0jnJ*I+lfJD>`gAU;{@TT=6Mn8sIf6fkofcGO{AVtfTk>0D#q75?
zE`PtI99X<NNwP=qf9=P>j9u36Z_Pd1`{yOsmyZ{}Yb!kob2(8uwPv~d$)BIRzI5CQ
zlrP-U*?U9({hn#vLR_vQMrxnet^B;KVb{uUQv_e6d_AsO^KVV(NwuSMoH>rIelevd
z#ph61{ob_=mvSO9-`z4dudnZ)(Y4a$TBS#5T5-VA8$BTx1t(wDKQzD2M)o^%riK3e
zh{LXPtNw-`UbNyx$egcgElG>C441w*sMUQk;lcFhq3d}TE2_9()7sF$wRh#oUmgcT
z`R_RgKI3dD*clbWmb$Ej<?g>zwW}BKahhaq^NE`1e$B7m^3*bwY{L}`<|{o<lw9<o
z=iffHJ#9gv&Z<Wv)2DAfc`#gc&J`gGjTP(cYDI3(sC!ru-BNwGre;lYtnp;Ej<4ZA
zt~Dfe2b?e}U`yZhVeOI&l7-(5Zg9MuGGkv|-Gz7kK4sr#$|Y=1?$T!9U)V8|EmcX{
zs8wWzj5c?{g2~@D&Z}Rr&10KczRVfL%3D7zRi{abOk8|IR9l&W+d9BoVXn~Cv(d-$
z1awMP&Fa1EVf4SG@0^9Spi!r;i9d^WziFMh-)GLfrvrO^ST1TPhizT7^iArz>W~;I
z<CPD+?%k<%oO0&f_SgyE0@7L@99`9P@|I`zUM>$aug_~w#f26YyURbRfB5d-#Cq-T
z`|GOybmr$rPp*Fu7EyHn+V_=**Yw_aBl;q4;<r1S4;YI6`|?4P>j``K+ag=@_UV5w
zo!(b{bKc%J-|xO}tK@oNA$e<EjrP4q3%t*+$Zk}r4`JD8Bf5CG(!VIK=Y|twTZ;Rx
zER)`{FIwKuJ=Wa3?EdD!Tki5jLQSvh8RrP|#VsoBJDF1CcjRo^{HNim7J6o{WHfc{
z)}A@Af7ezgM#YvHI}4cC?TA^sdgC*uusdBFZrpM{I(z^6n=&4$tC@=~@tI1Vzsaiq
z#&mj=lJ4<s{l(YLF^lM`R75_w{dxK2rK``L$)0^EJ>9TPbIZ4)h>X>Hz1#K_YDur(
zEOxzq+9ZK6p<}P6Z?yPQ{yEGsk>e3tmu1PmWwU(0nsv9Zf1IU#bkm+6hVRcl^KCZS
z5fZdkf<?BFeXin^n^T;(3N$NUI)5d2gZo2XCvz3EX)}0P);V6WbU1O1({7gLhNkCA
zCPCZho{hdVYrWW!g-Xd+&N;6T?9i2bl65iUwd7R4Zi)K25|uLyt!GSAUDCPleF1;+
zcC+dN<z;m{Ub{~CzphXsLYw{2(dG|3LR$EaMey8uu;E5j%W@mzkmt|$&av2YyYPqb
zt1U-whQ633FBT};wUt+R)sE879Ou6(EtY=yz44;%q<vvmHLpr%K6;@xnful<5wE_5
zPlZzgt}T4(v5_m|>(2Vb>6U)UH&We|?B{Gcaa!Wi8?W!)^P<)+TA`kv;H_?OX?{bY
zz^rDOBGoU9-4{7GOVmu%kUo&^t(}+?RTh-NcWgeB*Zi1sH7a}irp%jg=@pCCT0800
zicTjT#T7QJ=}!7M)rtEd>zZ3G$3$DMEt)mkoPE)cscK=TT4fnK-DhThsCQgwvGk~z
zt3Rvx^(`0I+z;Nu;2-YyG3BX<_%xsU-qVkLHGZ}1?whufsmmIU{yVnu+P{0d@9wRy
zi}<YV&(_KQIARWmc75Z~cjBoNy%#<T@!e>!r$w&nF2~>fJhq(^t{)P)808UBVyMf>
zs52?gyY$yjZw`~`3nz!ZJ89Fq`cB=k`eil$Pi;IU`1iFq+np~vUg@2<asT38N!dBi
zUQAgV78%N`y0(OSj=-%`i*}wBwYQn_d+sK^`X%w-<}B1aweDebIg|HtclVf#Z6_XV
zfBur~(>1|`uk+cTA51KIv_kTPp|p#MtNV(SE(<ljExYE(Uj0yZde6p_CHM7Se#vgF
zV7L^}TYq^c%eO_lN<&^)OzgK?eW=FLHtXiGWpQos_7To!R+RFxYBvj}vP?bM+@vL^
z8&PlB`sRVid5#aWU9vfj-Cm*dM9Hh$_EgWOgW2noKHc1XdXWi#&8oA}M{+d;m|k`T
zx~ksWr+!#quj2b49@Tl4e~nwjl8(J<I2g^8FYuqIWZR?qy-KdE0;|t#ov~R^b5lq9
z#l`B5v#PdB?XPI{;5+wf0f(ukMrUpBv_-<_*Ji25oQ%2Vr7jo3d~#0A_e5#lZo4S~
z){dN3>ZiWgUFDPBED`)mYq62V(>2ZqHKI9qWm8?7qs#o%WRqT6TzbA{{?~mkrtJK%
z^p1ZokG{{A$}qoJp88h-b!#^7{+d_*`lrwD4+{^9%P(x4%qln6)@%Eu=hJxCWS#u^
zGwb&J>Sy_k#~hm(eRoC)gsxq4($PjF=;*H%LeDmD-KTDH>15QqXT1#;0V}mqr+Y7r
zTJs`H_CUtssCC)C&o(K@HqG+RdT{oE>MxJ<Ef;D`ykxRlE(D2cxvnp^t&g{|a(~fq
z;)Q~&)&Js3n@c?x;!E_bzDks3OFq03yw8rQCg9Lz1)1FMznB)?Pd{RlZ}6{pP1>xi
zN9Uy0E;5WUR?=QOVU_7cmvDpDf=N?98?6+NFK^wtpucYl<C$YWj_?^ys)$ilP2yeN
z>Au{zwl`L+GC$j_$4o`iGxzBEB|-I5#M8Tig2Kz^%dLO+D((+I<J|LpXMTQqR(bI$
z$AsQ>DOua%&cuCUSXlAJ_4UnbeY0oJ&MZH^Wo44s1n&<!w%on4y;kJ%?zEq=n?L1=
zC;hIwWoT3%zJ8Ck?yP&Er{AC3?0;uU`<AWF-|k2_x=svAoPIKVlckroPTE7hLZ6kt
zLYCI=laESx_hVCD;{Rr+o9>HeRrKWsh`T+zll|h1@A<IXZl^sj&oqh8Fu4AhZR+>-
zzIj(xPkS9&Yji({`&6QRe)#(ZYlJUqh8#WWta9<wxocW}^DeL~*60_QdV7+b_`bB?
zx+nIyZ?f6q=JTgYWV_|nR{p!6XK!BqvwYv*D|u(*XT7NJx2#_D^to?n9KT=pHLl!?
zTba_ejm5Wynz^lQtT}zsTKZ9;jC=Q9qknU+y#4fFNpSV4wxhm!x3ZsIFk02IINa^w
zj?1f#zLr~lHmP0D!tue!_T!m7$MZ^7-~D?zczU7E+*38*|CKIpebW?hd-KJaDmi;h
zXQwW+wYplVHY2$=x4-^s+|*7c$)H5h+>(2#J+A+j&6#}W*rSe^k{XWQ_Y9M+#oFHa
z^WG!s-qy%33oqAM7MpnO)UtQfx)^B5u92{NQAng8n~nJWX}orCr;1K8oNl%|Cv3sx
z+tsbLO${$g%m15R_xIgCw|efoU%TEbO}r5mV$|r_I&1ECLw3X6=aww6sXzXF-L5$)
z-Z^6F8{dC2kUBf_ef!LBr}j<`JM6hypYs6s<96FR=d)W2PAp)Vy~a{)dh3z`&!cWU
z4d*$S&+D8M+pU@~GvfHST_*AxHoS9xewOGEU2sm>Lz(^E<osWS9DA1w`5jZNd1t}X
z@}N{vdGg^2$_w*m1Q}XN@rtgAkCL~qmv`HG=i0jF`{mtVCiorwrOnmxp7qFl9|QaO
z2`hN3b*6PSX(Z?L3QlTI;BD!6#WH8F((VOs?<sgSGX!>(&e_@V{rTLDBCB{MPc}Hq
zJ{RaUJE(hOW}y7eQtQWQWyiL;FSk0s>-oG{KE+G7aqazIe1TtJuc>O3o(R*n&mIkp
ztIpKhoD#jD_x`)(tlaxP|C=6uw+*<wdGbX5<V=6IW#8Awi}^%-JMDjPiK?lH<Lf!m
zaeIO$Zn^O?X48!<UaM^9s*_WHeNXae7H%wDuvgQH<L9y<*98uyR?I;WyM*(?$~W}1
zR7{-Izl!PCjAK2U-#1^*{+;Z>GwFW1L~mGzNyg_2pZe!Z)~cD;NX)*?URijt*x_M+
zAgh_t)+4u?h0O0ry}ghoT9felZSc>gZ$AIuXvV#7t$ATs)#v?br(EZSm}lFbHsyFE
zH2CDrxtg&h^y;d4FP!_2&r-kI{BmE>_pH(>GTV7<cy@A`a+@vdatl5+@!F-2cF|7z
zrvB@?b^hdWt#_NA)vxj56>}ByJv6I}zx&IpLrZS%Vf0|>X9?&kY;>}ozd$I|*({Su
zUcv5j$h7rKPwlgt=gi|^xyWyh%hJl8FzNS69Lua2V*Q!R&HKAQ8m<k_uU@|3UX8Bt
zSKGqVrYolk%%4|z_@qsw@Y*B4)12<Cxcsz=t?OpN6}1;rWTl&r9iLF|b>dpZ;hk}J
zj%4yJe6;-BlG$pv=UZpH+-ZN}WFi<Kkq}+X{irKSG&{_!W%W|!>N5{BRxLeTQ&ujv
zy`yMJ(=iv<Q-Rh`oiZwxNJ*BfC&c)k-D=%d&Z&Ik=0R_XwcD6ah_2UBbeqdD<y)wA
zaPQ{M#TECJLwDLot^0m9cCUqEd3|=^XP;liN5rSq>U}%-&g09LgtYWMDQ`dYzZ2a3
z$3r|Y(k3$1Bg*F8qR@v*HtSSY3v+pi1t@Dq-19Ekc*?G5vvu{$6Z;Djc^BHZtbCnT
ze<A$U`keaGkjP!vKN?K?wk=`K(aWDs|JJk8{TA4we63?bk?Dy?$<_Mn%)&j)I=0r-
zCp~_~^=tNa)~g3PZcPeOlDHQxTK;pRri;h1nTOK7FC1Si9Uu0_{JzNt<~Myd9GxOd
zGu9?<SUTyr(3bOFbKaB&R<(VLR1(~EKIv7r|Cf;T7V+y#_h0hh<x4VjJ+pM3+EOix
ziOk!aG^a!?7i)`9SggA+(=XJ@Yvbu;sn~blbsq=1+&<sF(f`t{sob8kLtehybpKY;
zFO{{<Vb@Y8Z#7nuowIhq;o=iB95i+<KeFqDzpkXE70YA=@k{f2FYFHPh+3T~yKrNh
ztAm@?O`|Je3YT}^*)mx}Kug~{Ix5Hg^^33f`Lx&77b<+QN<X(P<#F(~9rvr}g(!wh
zJ!5QqA$-}6cjsPRshi(tF}YDdMd9O>&n@S}IiD|J;0`ThUA*G$iAPQyQ?+$odG@G$
zc*?SR@=*b8rZ2B1e-hBG_Y?5zTBsUf-4iq4{N}Z9`}~gY+?!`@Zs8*IRM&1z`WL0(
zK$$FqRX??M+D%+*&wH@a?m{B}yJuUIEmLy0mT8(RNd_(Gn9&l=CHUabIs3%>`{pcO
zE4ysRPqRe%Re3u%oD&Y@{+1FuDL69Rds_CU^EW%c9g<nM@_byVN!hkV)6*u;6_l^f
zvv=k{aa7>mtR?F$70yn55p}n#%0Jn4!LRgdObv7G_h)bW|0j+AV8>H+){E)d_oAFS
zu1>p9<S+f3FP&p=^!Js^Oiz_sJUFuM#>@>m-;1BESo^WDK2NWyis_G1-E@!b{Sw-)
z&!<k8Y`gecLSu!N!%~qmpAOENKILF^b8*J=ro?)q#+$cuRux_C%I9{Q;UK!=Tv&XZ
z+wy&C673lhJ;|3g=1TEd{dll5Ek9f9D*LaV|G5Y5=brwjbf<mF(XP+}p0`&PO_<H#
zdR)V2lB@B@MIyG&+3#7urM$nJzM?ZfU4w0{iDMc=_EG&#GpU_9>W^RR?29gWEvfro
zEnCr9;qb~RM}?`WO$YNl`}ZD-I?&iO`7h^PsdR4fa<hZ+Y^T>Xr|uWfxy^U@*0*!l
e-xRF5dgj(U!I(Oh>J#n%nXk@x{Yp89fdK#jt7HcN

delta 4582
zcmX@1_DhvVzMF#q4F123naE>apQ}7Gt$g#z!%0_HCQV$I@peU9gjQnftE`ZjTq5sh
zFn)aHzOV9!=H0))Uf(@Fzizkw*Ju4}Z@pUkaCZNv->>AOJ*qxGe)vlEf7NIA-yiS)
zzqRTk=ib(%MVnjY`NZ#kZ>@>8`}gO^>9D!?uX>l?SKZqB`e5bbE_1F6yWaR-Ir>Xv
zW_^;5=WT)YQT}=F?f%8c$xW}?(t5Vo>i6MO#%npZiL8kWjosRnaU(n|hvjyV#fDYk
zxBu^0RsKDE`^)XKmq#UE-}l%*@n;@)^!>lvY>jGvKC|$7{P_QkTT9j-Pdfg;^#977
zyj@M%`)V~Ve?7bJ!H4~KAN%+0eS4aHx^jkFf1htrS3P&rx|m5HTWdO>zWVm=-S*Y9
z`}cqT%UfSFCEmPW+d<`P;*{32H<BgSxH1}Ez8a=)zi2(X-<gcwj($#=NnL6;Qf_J{
zh1yhR`s>x7s9*o%-@O0NweHpanjzmel_REGbT|LpivGnHPVW(Y7%lLv_Twgr8?UFo
z-`C5vIDPI^?W0eY)Yr6SY20r4wEcqc-S4MGfAiN)kK-2GCo!MrN>+n{#bX7n>CI;f
zk`)=>sD9O0zH`a%LyvtbH?Fjt`u}P1X8ES4iI%#ud!7bu?p6KKqL-0=()FkoOS{x$
z>$zu*GWehVE3ezL^Y@Nb_u^DVsu}m%O~1fsXpt%uP|9;MG%3G1-0XV2z#hGKueR@Q
zKVI_P@V-po&J0nt=-;anc31=+&3lzIMZ7rIwM=9B8iy9Gu=!IZ{K~h?-dN+a-=?fM
zW6s0Pol|#7&inF7xk^M`Z+ky~?D75o-^Kq{n)&pkZ@=tn%YO~8Hy$$CBs8Oz#m|oE
zxxAt0zj?JOYtH+~ODd(k*HU}GCbeF6ZTp*$kS+t({Eae!LJ#VbFS>2-Z`yUU&$d?I
zR>*X__Oyc%AMcCHw=UcLdEMQccTUV-=O8a%yI;vE&$T5c{A796lsWqAUHVtZeid||
zeWT;=r*qjmH5LZAC?*@dpJkQLwPJRbzht9dSbfZ)=jUh5$O$@Q*^;oQ%kQMeF_oOF
z^|!e+&bCc`wyw7L^Y`x^D`$A6%xw=zHDeF$I_n`SYiRjb>CemKmkaGDw0-{6X&Q57
z<@I_~ovtpwqmlVe8fvSAg1h9_Y?{HtR#zGK^^}2>Q&GxVChip%X3tvFFB0?hfvrgD
zJO_^HtB<Azq<Ohtc)R}2cCJ?w944ooULsnV@^(u7;vBC{V$EE?G>hb>DRP~E@jm-d
zwnnI7NYI?pGRxUAHKB(*bsL+TUcI{PzOnbEc;9x{9oNquKW=r+)Ht&#qP{hsS7RGT
zs}6H|fg1OHFRr<Q<^0XP6Z|?~zJAXB_TPz=^!YCt%dD5}VEQ1?H6t@XZIfcKN8_oD
zn;6)wGUZ=$)@OC6WPd((P-fEdx$}dQRyqn=cExNoV%o5Qc`M5$&A_{RQs1y0bXvaZ
zrbVyHXaDCfdNvCxPQKyv*=570h{xrRP3B+NEpzpRi$JeYQmA&+skmpm+>b6boGi8O
z$=SQ&E+^mAy=~gkZluhjA13N^%`fV8sKchfS^1&gR&~v`{-wZQU;e%SPxQ|JUoSuQ
zuc^L0>ksqxLz8}Q+vhKvmU|>^y~FpeEzjq%_O1M|yxl)g!G1^9^w&Er_q>@N_wDZK
zZ*Nlfzppbt6YOyO<b|@Q(I3UwW3$|1xmA8HR_b`VQo>gB<Mkkm{?0c_bBdRk-CgkY
z?ymx?SG#s@{5`MtlHIQflLcb<>mST1_#m{l*hg)0u~MGdZyo!o4|m*HQM_c!k1a;b
z|6g6>Vr>yfdUl9+$D^XH>yFLhjwsYVl$6acn*VQKTCu{^wR|T$t*@lmq>Jy_a6Klg
zbBoMvyK|A&`~h1gJV<TKKR@4Z`Z_b?^|@U0=N^?<cH!3P#D#0W=}CS%wlZhWxu}@v
zdM~F4Pl?s>#~xj{e>R%6Rk1@_<JpCuv$D*t-qsP4JCeOl<n*UU$M=}eHs`(cAjorT
zl0eB3*^;(^v|zrgPCR`c_QC!K<yy@-?oPN7kz^*YgDvnmgJQJ$kBnspxaM_V@VHxM
zmhYLpFG`@jt0&N!f1#Vgwv-90U4z%Ahgj(*mDDFaNj&x@A!^zLwO{)V+xFbO_2yvj
zj9(Aei97z=eJn9ytqg}a|Dnf0f>sjAh8fL=ld=WpeL52`cmDUHM<4QzKlER5Su8z#
zVRl`FOQ^;*GoKZYuANo3x!&EAx8y#%+jfs%QK8F2@|Scjp6#QTF*``ZvTd6G1joqs
zY05{n7F>PaRv-J!qBn86Z0DbXQ%d^D9-FoA>Q`oM?OHT%PNVMJ10MBE#~d^GicU<u
zz^>z_ekSRI>!KWn`MPUcHfG-RTxcm#&!tgYWchjG7ptHuC$H7QE4KW~S<}X$${yQr
zV3S_g(Qq!^7V!;P!jj<vQQcX2_hdRAh0lu66fa{@kxN~7kiEY3(G;<05nItaF_+yo
z*ZE&$vWc}kI(cevOoUObeyr5>^DAbTZI-?iI*Uo{xAgI--_`HSzW@7~cy_&wq>5Zm
za-q_iKg?pg<EOalwRQ!Y9zFCysOm+j@|XWcUsRmpxPx7?6%#KW-J-&>!DE;1)tArp
z6)(iJ`GxIN|7^0Z=(ptT`cHqgk88PqSsyP^aQX47-3rO|?%&f&3T7=1-WHV_YC2`h
zCEWt24DIe`X5oK61iULhwd>Esx|_vq%QSYk<=^GhnJXt-xbUV@^Zj|trB6h=x2)SQ
zJBPjfWar{Eh2uE_7e!<jPSSid!{WlLqOy>~w{<@sQ@dQdd&%YXqK_CooK5}ep9|gS
zeswKy;bRxOUu(ENKmD>IReE-nWZmBcUc<%LOhwl4xJ?lZQRC-YRk0=E?^BUY&A~Rx
z2l9p1DoW%p-ZY_GL-(78@hSH8d%I4izt`)&Wb<LAS-#-*g$^7`wB1CfR{WmF<NT#<
zkGJ8Jif3QW3q*BDu4ZP-=iKA?$N0j{uJ83-BBBm!jIJl0b6avkX`XBUJeJH?ceDOH
z5>>LaSlz62Wyu1SZ>CXQem2`z%`H$Zj?|u85x}cbTy(cR*F@)6fYVzR)faO#F8>a(
z&N-9h^Ky01sRvUw^RX_@Q8X!;BFdY0({g4>$I{0h^EcOB`@Jam*`eu0_NGRA3@$#4
zv@A7TQSbb7<GFX&cHdq5-1zO`cDDGM7B)Yzijr>{cfICCn{8O7`uzFo-1>Jj_p?f{
z^Rk&d&2kLcx=D@wV}OU~>&0F(&R_dA?}CSV_RiVnOphFvu9_07H#KYHqSd7gi+i(n
zt}~r^x~YUCOK)YPdGqua%5yI|eZHtsxJJ;)J9LG}-g94T>R-N)S;(xkxVhxTpYu;Y
zdKf#^U)=fPO7e}hsV%|&KYww2aOCuFF4%JSHFrnde8JCq4*od5aaQK4PV4L~UB?Q}
zcC6XrwCb9RaO^>mL!M#hPA`e8xhs0D$<8W>%|QCGu=Np-M}<?TbePUjlbdVy)wC?~
z$=<a$4Q@?HQQ0bLKiMm=K5mYtmuKwV+NwRfR#$(tXDP9>Hhg}1_H)<i$_{3`Cat_#
zWmtWZx#iJC@wMsE)_Hk(%kIivUe*=qpm*@`rLy4r-vWK!&w5&Z_SEj!j<>%vkDvGx
zyZ6(&Eg4ney8Erq+Z6`OUAo41%Ie_K0MY-f6J1&@qgPiLBr*3cvRM`~_4cHCIq_Ku
zzyEIi^I_$w^`9;*sZi=yo>nZ!F2C!!dAk4S_cgy)-kr7I<Yrm%Hy3Za*{k-*&6%bt
zd8;dl^<3Byp{=22ZfhHBye+IXj?|jut{3eu+G4ril4(ua<-F;4#5yBF&2;P%F2)(R
zPt$Xe*=xjgJl926;;Y5m7ORqjoJ{@pHuZj+%ip+dpK{yYwp8-?rIlyO-^Z5+=fwPe
zXO(*1Eq#u6a{Y7f1Iui!u2wE9Iwp0SZP8zwsW%Om9MZb=V$W%b?mym^>ViKWb;Oj^
zbo_qDFzH&X?VUgGGbY~OYO{*}?v-;h7YCjS{VBafNOo#*1JgEbuc=RcwikcQU3u=Z
zTfoKz#r2t+Pg@CFE!}e6O`T&#oZ;8_;+2z2w$I%i^6uBJ_ev8bghCd5@NAtm_q!qc
zM$L0e7T6qruBSO?2~&<(`o{N@cxLg=&;PdLT}A8c_r|xMiml;3!2P)0w$AzN)`AlY
zSZ1%WRGWU3so3+V8&AXej>2<SUW)Dh>N_*y__tjq@)|b1-1R?;+3#}&JbyTG;)Aa<
zRsUMF%xi0(T*xusnvYqrBKE|ICk9VEDma&g`1H9sv%a1#R)4-dP<Q***AKqm<uX|k
zyzyTb)1zv}kLto_&Z|pg9hU1}x=7)aM09e?L4^or#YI+(>FZDEW$ZTZxTN4PB}q12
z@6oM_be+~LXE&n<0mm)tT^9QmaF?ZBanHMZZpX~I8{b}Bd2aK&oy*lO$E;lI^!~rh
z7iO1y-_B{=tqpHC@FpzKGVU*8-Ew+%WMA5C^UM1ae$?_``SK>^$>E4wlN(?DeLbCZ
z^0c|<f(<e~d0j79J)ibvZHS6)nbmZiZBfnVZgte}d7%EM+HlFi&I1+~?up3Ox6}l$
zR0>!iHJ4FS=k7<{)whk^oc4H}bPr|Rd)V&ro8Kp1-+IO`)coZ8OXJ0&QoOfpZd|BT
zSgrkC{@Al`f<7@{WCDI9hcx#3=x+SB;K=bUZq{2OS><n3{SGmjV|&@Yy6bwiqI^})
zyvLJj*10R0OyBudUE$-5gA6n8SggMI$a8gl)K%fy7at=&FR3!P8~!eCZQrEF)8g6`
z!xyF<JQi{>!^`qg)ViDL-Y2$SiVys4`7`2Z?6o<eD-SL@vB)zb_+#S4xY!vcv&|Vg
zA53KMGSmymnEhTm&@^ST+6Tr*#{DusqgK6n{n+vd!xZILM?6Dj9naYMQLimw74wC!
zCR(MRcSzL#xoGuuTX|Q+S@Bmv_l38|OpfY|e>u~9&Y8)k7rhL!)sFO9#jZ<VFoV}U
zx5@A3M#GF6o|P>*z2<XXAC>KTCcs|%>cG~_O@DVbn;fb2&~p)HY-QZWx>RA^iqMT|
zsm?p1too11oQsXJTA5a!Uie?xT`R*UWQojHWto;X_f-=M>&y2XzIr8QcXGvagQmH%
zds;4LSvSOdJSCKLrPCoZeyj0Si`f=k-))1Y{$BjF>i(Up-NHrNFBtg?+q>5!`aVvQ
zf79pUzuK|vnD;fmZ7<|Dp6)LZoO(3bxoyeO$9hqsdWRl+ZL(UpAcfI%Qq$93Bk|R5
zl+AZHxAy&!7H4|$m(y7`*8F$ynxOjB->Vm&y0o{iedCtxtdDi(T@$<KpPMnck6*k#
z{1Ml$+1pvK9_Y9=DM(4;Ubtxa$@!Wt9>-=LN`Jljcrj;u*c<cvCLfsJeEZz)(iODj
zn!$~rlgXU7(pCMw?b5Jy{;e~S<L>eoUyiC*tuj8;-Mub8a|s*!#u-Y_g2E>UiOxB}
z7`;%$YfUh>v(AKz)7Ba<*OFa&L-l2k-uK_r{1)oIeSY{xy29C0txJ4Ym6YFnf7_sz
z?ULft7n@GrlAOqQF6_cX%M>34k-Nc3u}|_R2MS1YTv{KdaC!HU)sssEw3ttyjGVks
zKwLCpZir&Y)HBAHSBEd#@s4lNmAd)a=9A9~s3_b#{W<4YIOp>P4BVlGtczE?J@Lq?
zW2&~!E6*O44^Q7LoGd7)&2;DCWII7!;lAU(T?<qBt$SkTo8P=<R_2#Jb#k4cq-&QQ
zZ)23;PrKTmrAd}4xm(LL&6OmB7Ie&LiRKb~aOj+U;{APd7O$Nvvg4;&qWr47&UxpA
z1G&GY#7+v14ELUvz3KeTw6Bxz3hLDBMeb*RlEjhkd+EB&glAqQYx7+9F5jpW@Ygt-
z@xZzH_f2ot*KKZ3IPz(7(~Hfb`MQcnvb-}or}oyi8@JqB`#a>a)Ke>&f~4>_J`vM?
zTNYor_TzxPxwxY(W1ZlB?<Ke0d!{b>eCjmM;TNSmA|av+g1FLtUOC}?>cQHBmRp?H
z8`RG{@Fv$RbZ6Gl?X1c^3%EkkSL^F94vrV@aW>&OX87_(*%3C`nh!CXx0_CV#aw%A
z=8yXAy1%;%<b%Yt!wwp5QLc2#V-k^FY~U$&_DFZo7oN3y#cxdRO`X3`ZQtC55?d~@
z%w$|6x?km1#*<C5zt?U4k#})z`j$Vl*R=99@+{A4bO@Qo$+lb7_8V6=BRiMhr1!f`
z&xz^1%W2xrGcA_=be&?vwz*%nyq&xL=1Kq6Gq>JV-tmXy+XVjq>|&nZ6dAG^7yz6I
B^o{@k

diff --git a/examples/vstte10_aqueue.mlw b/examples/vstte10_aqueue.mlw
index e0f73dbc25..52657bc445 100644
--- a/examples/vstte10_aqueue.mlw
+++ b/examples/vstte10_aqueue.mlw
@@ -15,20 +15,19 @@ module AmortizedQueue
   type queue 'a = { front: list 'a; lenf: int;
                     rear : list 'a; lenr: int; }
     invariant { length front = lenf >= length rear = lenr }
+    by { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
 
   function sequence (q: queue 'a) : list 'a =
     q.front ++ reverse q.rear
 
-  let empty () ensures { sequence result = Nil }
-  = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a
+  let empty () : queue 'a
+    ensures { sequence result = Nil }
+  = { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
 
   let head (q: queue 'a)
     requires { sequence q <> Nil }
     ensures { hd (sequence q) = Some result }
-  = match q.front with
-      | Nil      -> absurd
-      | Cons x _ -> x
-    end
+  = let Cons x _ = q.front in x
 
   let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
     requires { lf = length f /\ lr = length r }
@@ -42,10 +41,8 @@ module AmortizedQueue
   let tail (q: queue 'a)
     requires { sequence q <> Nil }
     ensures { tl (sequence q) = Some (sequence result) }
-  = match q.front with
-      | Nil      -> absurd
-      | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
-    end
+  = let Cons _ r = q.front in
+    create r (q.lenf - 1) q.rear q.lenr
 
   let enqueue (x: 'a) (q: queue 'a)
     ensures { sequence result = sequence q ++ Cons x Nil }
diff --git a/examples/vstte10_aqueue/why3session.xml b/examples/vstte10_aqueue/why3session.xml
index 7a65b50b88..8c5dbb4b0f 100644
--- a/examples/vstte10_aqueue/why3session.xml
+++ b/examples/vstte10_aqueue/why3session.xml
@@ -4,7 +4,10 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../vstte10_aqueue.mlw" expanded="true">
-<theory name="AmortizedQueue" sum="e8b19e04718a27bcfcea7f31fb6f872e" expanded="true">
+<theory name="AmortizedQueue" sum="5e3861c4755d0109a04d27e7daea0ce2" expanded="true">
+ <goal name="VC queue" expl="VC for queue" expanded="true">
+ <proof prover="0" timelimit="5"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
  <goal name="VC empty" expl="VC for empty" expanded="true">
  <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
  </goal>
diff --git a/examples/vstte10_aqueue/why3shapes.gz b/examples/vstte10_aqueue/why3shapes.gz
index d78e6714d95f5b66566acf09fea48ee3b79f394d..898b2a14086ecc29f4b4b059ddec51056862da44 100644
GIT binary patch
literal 480
zcmb2|=3oGW|Ggon^A;P3+<mUSso!naF|#&T_bw$x*Hyb#KG`dOoj1rUjbpCQ|9#V$
z*yiZ$a=P(sPPLp`MSE+&waWLW?j*-Wy|kSiq@gz>Ji7KqoA>U&zZ>N<Ua4LAzuo^?
z&)MkmOAiw4*Zr+45}5w|q~qtH`LZ_O`+Ykjm)UI2SelZm*nC>XU5uwfKBS}N$G_#j
zdo042FiN#sy>{&L{u7p-cksrdg;P`7HrNT@^1gggF>LANe-V??7B6rVW%qo?nZ9X(
z(Y)t(*s4x?2k(k`cFA{@Uq+3K)z3)r8P`u+pR|@+mOHC|_Ti;FUq$cux>#=4(bu0f
znELd;t2x>SZ)Fq<(c?PW*r?FoX+48UX7Nd#@Inpud8HNn%Ey-8?GuRp)Bbkr{0(ut
z_21nQx2=6tf8>(SXOqt3E}UmSZEkc+*X&FyztCcF^k#7QZ!6ED#X8H6HE-5A5hU^;
zx50<&l}0SX`$H+g>930aY_nc|Q`gF>eTPool@sc{&3r%lzAigH<@%=OY<=$Om4`oH
zSD0fow@Oni!(Ov<%b|r&&P3&TY;;ZdB0hn^a*^q=<G*jLsb}PmGFrcJ;mQsB*7SEB
peZFUP$ep|m4QC%+I`Ein{*p=0CjPo@5SF`-L26gdu172k3;@J^@819b

literal 447
zcmb2|=3oGW|GmM!*^dnb_C61PA}8i1zwM2)xYq#zjlCiz)7=*LDwdYXmhb-ied=S6
zzNbOok`BLkd3H~wziHt*nawHPO;<x7PF$?;jMw7%)bQxN_kR`dUwZxi;r2}H`~Pm+
z&EWo9xtPzh`1754d@Jh~t-CJs&@i;hXyKywT8xjUOWdEoTd^Txv%_DhKB=@j=h<6A
z;us|lUA8#=b@NKwD_fsxa4y}fu~)Y<F*oarOlL|+smf!a%NNh?I<RL>eDj{e_xf7|
zh1*2Z>fh=8s-072B@^`Yr5Y>W`PZQbJ95nq?9obH%3?4f@p2+lzLrDVvMo-DGQ5YM
zu|-`z5uLf6yT|tL(tk$hZtB@i(B^+~!>(AdFmsvfyW`h;H<^9EzRYaab6=C_K=xx9
zuWszB%rUk%pTr$n7;u7n(kh*U4Mt9t>`b|=HtRACHe07zJmtHmYP$K8-C@ra9Zu?o
z1*P9&&&TOMJ#KUF!satC|0hQ|d@x%UqIT$ir&pqCkm8K3hYYlJ8H+>27*r>k9$UKo
zW@~l+{j}6|8#UK%sM!&J)cedj^POAnZecL<KAr2&uH?l#D}U|!*GXre2{YYRudHQZ
GU;qFL)z_E+

diff --git a/examples/vstte12_ring_buffer.mlw b/examples/vstte12_ring_buffer.mlw
index 376c6c529b..3c9436b9ce 100644
--- a/examples/vstte12_ring_buffer.mlw
+++ b/examples/vstte12_ring_buffer.mlw
@@ -32,6 +32,7 @@ module RingBuffer
       (0 <= first + i - size ->
          nth i sequence = Some data[first + i - size])
   }
+  by { first = 0; len = 0; data = make 1 (any 'a); sequence = Nil }
 
   (* total capacity of the buffer *)
   function size (b: buffer 'a) : int = Array.length b.data
@@ -165,6 +166,7 @@ module RingBufferSeq
       (0 <= first + i - size ->
          S.get sequence i = data[first + i - size])
   }
+  by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }
 
   (* total capacity of the buffer *)
   function size (b: buffer 'a) : int = Array.length b.data
diff --git a/examples/vstte12_ring_buffer/why3session.xml b/examples/vstte12_ring_buffer/why3session.xml
index 3f56401f04..8a2441171c 100644
--- a/examples/vstte12_ring_buffer/why3session.xml
+++ b/examples/vstte12_ring_buffer/why3session.xml
@@ -8,7 +8,10 @@
 <prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../vstte12_ring_buffer.mlw" expanded="true">
-<theory name="RingBuffer" sum="cf1afa8caf43dc4f538c9078462662fe" expanded="true">
+<theory name="RingBuffer" sum="440c787407edb5055e7ccec38c6dd29c" expanded="true">
+ <goal name="VC buffer" expl="VC for buffer">
+ <proof prover="4"><result status="valid" time="0.00" steps="8"/></proof>
+ </goal>
  <goal name="VC create" expl="VC for create">
  <proof prover="4"><result status="valid" time="0.00" steps="24"/></proof>
  </goal>
@@ -577,7 +580,10 @@
  <proof prover="4"><result status="valid" time="0.08" steps="499"/></proof>
  </goal>
 </theory>
-<theory name="RingBufferSeq" sum="2e16fc317b01f2605ce592d18305265a">
+<theory name="RingBufferSeq" sum="d5baed0f88a0b4cbc04d03e2e7c91df4">
+ <goal name="VC buffer" expl="VC for buffer">
+ <proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
+ </goal>
  <goal name="VC create" expl="VC for create">
  <proof prover="4"><result status="valid" time="0.01" steps="23"/></proof>
  </goal>
diff --git a/examples/vstte12_ring_buffer/why3shapes.gz b/examples/vstte12_ring_buffer/why3shapes.gz
index 929ac9ee09425542e7b773b4cf4a97288303c287..3e92a4c3a9c0203c6163e1ea2d5d2a55420663b2 100644
GIT binary patch
literal 2369
zcmb2|=3oGW|4*ZGyJgIU{@vT3w7;D@Xlh81ql`gYYwHAk_P<X#+T$KGR$tq0z0dpI
z_4uzo{@bgn(sJUHsvjS{k(Ol=^fGX-jjCwCw;37>zo}^j&2rL8xoBa=HFxjJ_`6qr
zx6l5u@7gB;v)j9VzJ2C;<6YeMW#JFsf6w=>*!?qi!oSDU<&H7dOaK3`rzzQ1{`k0j
zoJwikk<<NiEA8uMy+35M*Yj2C=Cu60<*Y8v=Bd9|uh}Hi^mh5P=W|O}7Oc(a{&><=
z=Zsd^bnk;PMI7!emz+6w8@+wJ@z3kpo69cE{_y$P***J@pRGT=;o$DOr|;gKdC~Sv
za`BB;RjWl+yLXB&%#)KV=MH?|e<<<^pZy$GlXJG-Ig1a!{baF4=!gF~X8-dWy^lqR
z?=_35?O3(weAg<bReBSfN{+m2_?P7Vd7@7TM^1aJiS*&a4<Z@bV@-r?-#gtcvvd(Q
zI@%@T{gvycd+wId1+}eDmMyLhK6Ln(PDN$W;=Vajx~6?uMT?o=e9ck)wID+~=&Y4`
z!R?2)h4-X(2_Hy(`!}HY?Cxcb)2F>~G8EN55~Uz;HRyzOs1I9`$yJ|cf8YIm{Myvz
zmTdU1b&hs>cHOt@a-G|p|L<tY3(xZnO>&G^*I7Q_+o<C*i+_S%%D&K?oyi9tz77tk
zY!!czsBwTN>$$SfPp4fB*OI1m3TbygJ*1_v_KM)b>#9$}OK*JH@@bFA*RVYW{io}t
zmMk++&gd<;prmtizMJ&_moNC;&(_WPm@V_*e1UWyi|MAMT;D}fA*D?s+96tzA0DP{
zKKs=C=XW(5o0j|ekN*D7t*hy>J}9A6rI3CwG<$X9oEnp3BE0*gc2$=D-{JlJ_MV%$
z@3zmcs)$c?p5W9qO;+`7@D<M*QH_nJ*R0wN{qI%%f45=w*^|rC*f%D<&b5)+le7Qm
zzn<E2@3PgWTRz{Hq`vs~t=9N=cejh~yjUA8x%JlCyVJwoy;h4|R&YF4A<VAW&nkQy
z%e+uE<*+%T*8_e$`x|CdS|$5vwvt8ew%t`~{Hqzap0A(hSG3rVZR_Pw@!1<zt?5nO
zVrS(UBVS-@o9eg!gX!HR8s@(r9^m!+`Y?EE>bb)B?dgS<N50L=v$waJYE$quWKOYF
zl!nGjGmm{*nt@+_rhWgtTj{|cYnz-SKGVb=t8}f8c+$1)OTu^Omsw)Ad{sX=y?gdY
z6<+<?^}9c<u;D?T^o%oti4B!gI)3XJzew48L2{wxvap4#n4@|Gbh$!p`!6JNa-KMz
zxzY2$2A{po_i{o7#k1{hU5Pk3WBK>QMKc4f7rNw{Ovu0Oa&Ob*#IBRmb1$8JBK6Dc
zdh-1hOV55h(K2sq;MuYzQ&U&Z`F<p_Y3cc})Si_Uy$dX29Wv^@zUT;W-D}=1;$<Z0
z7_@l(v}PCO6<0mFcBVN$i&U7hxX8gx=Y-X&Sr;S|x{gF~>A$|J+S0bxPFT6ik#(_e
z={A*f8*j~$j1(4Msj79kHDGT??tPnp*bo5~?_VNQHtQ`(S=!cda>5lswmHB53*VAI
zYv#}Ld!2)iRmJnE-@_)0rm65P?|8aCao>Zi^PCG?R?V7mV%MSzY#TB}q|Qn8>Nfso
z(EJr9kfa{ga?+zTZpulo6%)ej8df#fS^jyn<)h{!wJR6B1;auFtz;)N&-eNCWKu$?
zu2bx_W5OQpq0fJ>*nHihY{~!J-pY=z-hy&o4Xr%Slo-BT-@Ig9z@#%zo11b1vrf&}
zDs8d&N$qi_i&t+qr*Rh@dmFnz;>fNG`+jRP-Dz!jqOfC5mjwSVof{U4*Zo4TJUJce
zFC7*=^-JAbmn;dZ*Om7!A9K{VPwe~{o_^@=%dX#@6)(3H+&(tvXW3@W3oTwHCs;jR
zzftLQ^_aLwX#!7p$DU1AG0NAoxOi^e|NAE;^6W#i$VE4LHvVss?%>PqG%T19!)7Sr
z*t7bZ7FY3+Bd?sCeka!Z{Hk<NVU7F}>Av#yW_G`80V~(JtX*_v>%XX(>wi`{q=fo1
z&OE>x(kj4QrF};ua01hjW8J2+a$fD6F)>}~$pg(m$#?E6gIqnemo>3J*1OZH^Z2%T
zZ;1P0?u9#Mda2Edm?4uky?NVFiK4GnKR-rpJ}Z21ukjn>qNznbrv&6@wwhT9d5Lu1
zT*b}#)_B<;_4erJIR^VS7~T{4Xtu$wK!;&l)Z>sPug^qXE`3zKXWsQItI8@8GhG)4
z>Zh!$OkB7=-Az{cnuzZyvjko@et(5Ip`9;smL8BlzQ)v4{1JQFTKlHR|E>)0_Am&W
zis-XSPCe0>#5SSmh=uH&kC%5BSKOF({CK9+6sdRbgwi-{&2;2q`|DaGe_t?M)my+N
zb>Y#JiEcMG+!TCwziGNsaYL@+;jn|duSP8B%=v#q=YHWQp)#iBN+Bnz#kqe8Et>vD
z|JstPoK6P5IZJNr<(PQz-ZuWoedc?bIPP*OH7^%9>A6Kfvi!}N%sVG8EHqy(dUK=o
z@~Jby29{)ZTqwPkl|T2?yyCS2M!%wZRi&3i2#Ybex0F3C^!x6{^gNY$)85QJzhkqu
zUS?d+oAI?k$EGaN;rR08oO>-FKa}hd==DF&ExDEJ-r8eK^9>g)oS1(7>7w3GVX4~5
zsyD+=d7bJLYTK|jAU31n_trO6H-F8){kyF4lK#DK+y1N)UY?}B(k?>hQNb#W*u|{R
z7R)`obLZ<K;h4(bdEbBUxw=0>`c8q7flY7x>xR<{WSgCt?YK1`i70o3PWElwv+R?o
z)q_dl8hdow0yv)@2|4ykC&a{MLg>E)_B$sx)^^J6V9Z|I<~RBL#eZdK-~7~P+D8hM
zcx=3Q>bXo8TgVHo;(reOGVRCT)@BvFf6KLT<<&P%w{Hs`J}P>f@knciOQB-$T0M0$
z>ph>he@y9peBoVM^^UIO<4pc4)17>s`xE+P47KzoRnFDY+iqJhnW>v?mE&BtMQT@U
zmbMvcwoEl>&so`!_Mvae<)Du*jP|rt-~AGvdoJP-&sY2X|Nl)d+ua?ux;vugtl8?l
z$rln7uUoCLnxe7XpvhZi@1H<Z?~Id&cE?QGQgCYLv^8I3<o7b%bkG;~tZ$rIvzzVh
z$$~3>Tnf{)E)+9qb}pRc+R&mEx<G&@R(;uXjhC!b*xGIeT~+n^^j2!Ax^wVuop(>W
zj~`gmyMB`XQj291JT|vT1?x|~T)gGWBw5{ct!Fyl^QwG!8Fcks{S`wc-g$-$3;_7C
Bq6Yu~

literal 2258
zcmb2|=3oGW|4*ZG^QFy&{_Wd;=zh2M3CW@pjF*@k8JO9+>MRrX%XBfvOEY%9x#gw5
zGroTFC9l(0y}T~Z%T{j_WS0wk^5Nkg8|S{#l?7`vx<8(D)j6XTHr@MROc6);-`T6H
zs_Un|^S&`<L)7)F$5+cAa{l?&Idb`>*&jZ?y8GI5->>y2s!BIk?%io=xT`%ghi|rm
z&>WTbr*@fp`Zn#_Re$4*%ijCk>Jx9*77AUk_^z_Cm+$)JKd;Z;j$18v$Ugu6^bd7k
z3kCkao-TJ>@V~_W|LeSuMTqY;i>d8cwdj1;DyCI>6Pvai_cZxg`nhbIvS^u;<I@HG
zlI0h3c*>jA8Q+v$^!T!cyY%i;0pAlM+Ce&3wNvD`UJPseCOXMl=I(Bxchl1kex58{
z`s7N+%EFMz(y|Gw)3q;JyGBpUx@OsQn{U3{L)~B*M!oF(_E~$)*4KHwdb6O|yJX>v
zF3}`ifsQQACv&ybm<?xT@ja{k{_x>jA*Hw9v}>;`$ltrOPX5Ruzk}wrj|*OS`ZqMm
zF<xC~`Fw5T8JAh*6V9dV3(eV=eBj~Z<bcXX@fV322UxP6D+~Q}+Qo1!X-em<*-1M$
zaCvEOb$^k|`O{a{tTv)Ds;f#nZpYE5_PjyWs_~pr$}(SeS)RZ5&*at*|LXc1+20<w
z#6M>E&%gblM}V^SwQDM?97EMTHaabx#45io>~)OYsrRc3>gDZXkKX2g{pW*Bd6Qwp
z7l(6AtFMJITmH=G(Uht&Eh#Pky}@()>pi#D<Xw-is_@^S=%MI(x^L1q%~vY>xTf5Y
z%AR|82LHXP>g~7BzRC!m+#Ip-tC<{c+_t+(^@r@#zi(xqZuxXylKSG`w`RuY-Q6y_
z^I~nZ<knldcc+WJd(F2?=8$Z8W5mxhmM>#&3RQ&7?1?B0i*bIqnm_yGm6y34@4Fss
ziOPS~X|smyirjyjxli2Y@?<Svt!I`P8Yz7`qqbzy4!g%$zb07zJ#)Qe@}fIW+L_HQ
zuC@1vPP05-8$16<s`%~dU3E1jT9pq@t+aSvvLztkQtpJB(4a*xK3{!yIaaWsj{m#1
z;pCl1Ejk|^7h~qWb*cF--_q{L68jfl#dQqpUK_msDZ0IW)=kEy-FXQ{)h&$60+rtF
zKC@u*SEuxrXEUN&SMg;SI&IMi`D)^{TUABj{qmz~jE8N$@>OmQb&Xl`^YXG|UdL?q
z@(Q2rxy7lPwYah7mfELjb9sVgYHq6C^;x$tzu5L$Z`7?f{XQ=urLX3=M@4QsRp~!R
zHR4xJ=&>1H*EzZ_OSWuV?xN4M@PTcG_d*q6K^4<qS(Y9qO;No|W_X*W#IZP8YO$vr
zX<D;*73W;WWgcsme%KT@*E!?HD{jL@5+Me+Lejk-$*f*GbE0YC#Hd9^b2+bWzVYoW
z^Ho<?$4yK89W7rwd4*+l%;52qO+2vEe*T4jS=%brZj`eoT{>vJe$Vz<YYdbNEnIc}
z^L&;JulD3n4Y_*6<(g=#S%d513kBCQayb8pdtBV!Bw)Q!$;WNg=S4nYPOV!$F@~^y
zIr;FupY(j?JSW+`B8je|3ojd5emJS(ug4j7Rq0A)ZVf}``d20LrJtmZ_kG#F*06kI
zo!+5XPJ_t@Ls%N>th`@wsh*6n(>NivbXia2?nYy;d*wO;v3qPYwkf3FxyRb&sKfns
z_IkkwdMqmJ2cL!<sko4O@EGULvQ>-J;`OR-ZMd~)$#-w{pu-nD&tINr##i;1)w}1u
zmEgO+@H>7-inq7EHhbo?eYS6-TF4@2J%^}tbx$3qE)mhjlpRh_re1w0v@@*zz=FSL
z&!3-m^-bPn)h=I&-}*ZmUtE|b!OVU#Rlr&B$d0V_iwxX-)|^w>5`H`Rl0LJN=7~k;
zt-NCA+ZJqU^D0%%5?#9P>-1AKXZ4wtR%daYV9{Hk)go~r`k`BAlZb-ZytNlog7uH~
z*a$1K`*)ryu=kp(<rQTpY9mqpOfN<5{=Up5R#I^sN6&^BT|9E=iNS7}ExN}hte$?l
z-~FuFd6w_zHk>~Zddg7Kxh6&I)(a1fK$W!B=Tx@1`}{o5xBcABgqp<UJ(`bl6KWqs
zFyw4Kw$fwz%&p5#AIYz`UB5Ck_xqtsU2co#os9W>$jLw5O;-7ui0>)01YS3Oe}y@r
zoiB2h9;ok$%+As~Qhp}tKV#b8sSI~28P&2h;<${oCNdx8QFz)>Xl3!3|NXg#b+K}C
ze3utoDKLL-;QV4^;>Q<NU%1cQYVQloZAre+khZ+X<WSq$zJlLkHsUj7bBraoaoy87
z#w2^<TmRWlvg-PY>IGU(t$WHhF3?x3I{7cjH%eBKrM<IPWOurv(T&^R6i<I|6Bk$*
z?U3?8LdmjIOzH8rxt6`slDED-+oEJ$_I!)cWvz<M65V;6g1gQ|y<Ho8vv{4TlUw}i
zjVa9{*@u`C`Y$ZA@p*aA<AF`S!#4A?7f(iPF0p#Blu=i%ul4vjo{aw`J!fYdyqnjT
zzUbr23bn;y2WKCRcp%JXV)7}+%22#)(vha4O3RjXT{4YI;Jf9yb-vyGd!hI4=i2%H
z{(DMlPo3^;xi<Iv-g{#uw<H&297y;4J|~IAQh$@?gzF*m7Hrq9Y&~R=#4$C%&nI=w
zIVV?VmdK~)zm>_#-oAhFu4%&Bs~4O<O7zC6r@b$k^m8(+W4nm-+M06<GaOpi89hH=
zQeIdQaeo=x_j`H*)+T{-Ghf_Fw%BcRtI<NZSL0mDs;f^=q_vB``PNs~`S`+#)ao4_
z$;X-eRi-=nI)9JulQGoNn-n}pOK<z#Sa#O5wT{hJye^ZM+pP}M(EK>%$&s9u4QU_x
zrd&Ssv{dq5#oj!t_Aqsw#HL^O@7MqL-hDSx_+q5ayiJW6uO&<(PAt8*kWclLX3qm5
zcYXU+X`H%|60P2o#QJU?nUg;^DJoq-y5q9W+_MIg{iiRmmHu{>b8Gs_d>i!%N&H%o
zEFMAn;R^(KVwc4%KXFZR3fsFYlQvj-eR?UhG~M~YE}eHzyN@4O)4P6>{?a##CwOdb
nkqSP4d0lYJ>p8M#^=!^ee9!yk+0RKE-qn{H+60H`GcW)E(=$re

-- 
GitLab