From daf92378a747b0f72e0223807416ea7471d0f098 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Fumex?= Date: Wed, 14 Oct 2015 17:25:54 +0200 Subject: [PATCH] In a driver, add the possibility to remove all the locally defined axioms with a single "remove allprops". use remove allprops in the driver for bitvectors. --- drivers/cvc4_bv.gen | 48 ---------- drivers/smt-libv2-bv.gen | 96 +------------------- drivers/z3_432.drv | 50 +--------- examples/bitcount/why3session.xml | 37 ++++---- examples/bitcount/why3shapes.gz | Bin 8638 -> 8613 bytes examples/bitvector_examples/why3session.xml | 10 +- examples/bitvector_examples/why3shapes.gz | Bin 3032 -> 3023 bytes examples/bitwalker/why3session.xml | 10 +- examples/bitwalker/why3shapes.gz | Bin 8991 -> 9003 bytes examples/hackers-delight/why3session.xml | 22 ++--- examples/hackers-delight/why3shapes.gz | Bin 2850 -> 2847 bytes examples/queens_bv/why3session.xml | 12 +-- examples/queens_bv/why3shapes.gz | Bin 16134 -> 16139 bytes src/driver/driver.ml | 6 ++ src/driver/driver_ast.ml | 1 + src/driver/driver_lexer.mll | 1 + src/driver/driver_parser.mly | 3 +- src/whyml/mlw_driver.ml | 8 +- 18 files changed, 65 insertions(+), 239 deletions(-) diff --git a/drivers/cvc4_bv.gen b/drivers/cvc4_bv.gen index 4d4f86183..b28a7bdd8 100644 --- a/drivers/cvc4_bv.gen +++ b/drivers/cvc4_bv.gen @@ -4,67 +4,19 @@ theory bv.BV64 syntax converter of_int "(_ bv%1 64)" syntax function to_uint "(bv2nat %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV32 syntax converter of_int "(_ bv%1 32)" syntax function to_uint "(bv2nat %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV16 syntax converter of_int "(_ bv%1 16)" syntax function to_uint "(bv2nat %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV8 syntax converter of_int "(_ bv%1 8)" syntax function to_uint "(bv2nat %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end diff --git a/drivers/smt-libv2-bv.gen b/drivers/smt-libv2-bv.gen index 25fef8385..a30aee0e5 100644 --- a/drivers/smt-libv2-bv.gen +++ b/drivers/smt-libv2-bv.gen @@ -20,26 +20,7 @@ theory bv.BV_Gen syntax function asr_bv "(bvashr %1 %2)" syntax predicate eq "(= %1 %2)" - remove prop nth_out_of_bound - remove prop Nth_zero - remove prop Nth_ones - remove prop two_power_size_val - remove prop max_int_val - remove prop eq_sub_equiv - remove prop Extensionality - remove prop Nth_bw_or - remove prop Nth_bw_and - remove prop Nth_bw_xor - remove prop Nth_bw_not - remove prop Nth_rotate_left - remove prop Nth_rotate_right - remove prop Nth_bv_is_nth - remove prop Lsr_nth_low - remove prop Lsr_nth_high - remove prop Asr_nth_low - remove prop Asr_nth_high - remove prop Lsl_nth_low - remove prop Lsl_nth_high + remove allprops syntax predicate ult "(bvult %1 %2)" syntax predicate ule "(bvule %1 %2)" @@ -107,8 +88,7 @@ theory bv.BV8 end theory bv.BVConverter_Gen - remove prop toSmall_to_uint - remove prop toBig_to_uint + remove allprops end theory bv.BVConverter_32_64 @@ -142,75 +122,5 @@ theory bv.BVConverter_8_16 end theory bv.Pow2int - - remove prop Power_0 - remove prop Power_s - remove prop Power_1 - remove prop Power_sum - remove prop pow2pos - remove prop pow2_0 - remove prop pow2_1 - remove prop pow2_2 - remove prop pow2_3 - remove prop pow2_4 - remove prop pow2_5 - remove prop pow2_6 - remove prop pow2_7 - remove prop pow2_8 - remove prop pow2_9 - remove prop pow2_10 - remove prop pow2_11 - remove prop pow2_12 - remove prop pow2_13 - remove prop pow2_14 - remove prop pow2_15 - remove prop pow2_16 - remove prop pow2_17 - remove prop pow2_18 - remove prop pow2_19 - remove prop pow2_20 - remove prop pow2_21 - remove prop pow2_22 - remove prop pow2_23 - remove prop pow2_24 - remove prop pow2_25 - remove prop pow2_26 - remove prop pow2_27 - remove prop pow2_28 - remove prop pow2_29 - remove prop pow2_30 - remove prop pow2_31 - remove prop pow2_32 - remove prop pow2_33 - remove prop pow2_34 - remove prop pow2_35 - remove prop pow2_36 - remove prop pow2_37 - remove prop pow2_38 - remove prop pow2_39 - remove prop pow2_40 - remove prop pow2_41 - remove prop pow2_42 - remove prop pow2_43 - remove prop pow2_44 - remove prop pow2_45 - remove prop pow2_46 - remove prop pow2_47 - remove prop pow2_48 - remove prop pow2_49 - remove prop pow2_50 - remove prop pow2_51 - remove prop pow2_52 - remove prop pow2_53 - remove prop pow2_54 - remove prop pow2_55 - remove prop pow2_56 - remove prop pow2_57 - remove prop pow2_58 - remove prop pow2_59 - remove prop pow2_60 - remove prop pow2_61 - remove prop pow2_62 - remove prop pow2_63 - remove prop pow2_64 + remove allprops end diff --git a/drivers/z3_432.drv b/drivers/z3_432.drv index c559aa536..2e88431d0 100644 --- a/drivers/z3_432.drv +++ b/drivers/z3_432.drv @@ -28,7 +28,7 @@ transformation "eliminate_epsilon" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) -(* Prepare for counter-example query: get rid of some quantifiers (makes it +(* Prepare for counter-example query: get rid of some quantifiers (makes it possible to query model values of the variables in premises) and introduce counter-example projections *) transformation "prepare_for_counterexmp" @@ -82,67 +82,19 @@ end theory bv.BV64 syntax converter of_int "((_ int2bv 64) %1)" syntax function to_uint "(bv2int %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV32 syntax converter of_int "((_ int2bv 32) %1)" syntax function to_uint "(bv2int %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV16 syntax converter of_int "((_ int2bv 16) %1)" syntax function to_uint "(bv2int %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end theory bv.BV8 syntax converter of_int "((_ int2bv 8) %1)" syntax function to_uint "(bv2int %1)" - remove prop to_uint_of_int - remove prop to_uint_extensionality - remove prop to_uint_bounds - - remove prop to_uint_add - remove prop to_uint_sub - remove prop to_uint_neg - remove prop to_uint_mul - remove prop to_uint_udiv - remove prop to_uint_urem - remove prop to_uint_lsr - remove prop to_uint_lsl end diff --git a/examples/bitcount/why3session.xml b/examples/bitcount/why3session.xml index 266d41b5e..217bda969 100644 --- a/examples/bitcount/why3session.xml +++ b/examples/bitcount/why3session.xml @@ -7,7 +7,7 @@ - + @@ -86,7 +86,7 @@ - + @@ -177,7 +177,7 @@ - + @@ -262,7 +262,7 @@ - + @@ -357,7 +357,6 @@ - @@ -368,7 +367,7 @@ - + @@ -377,8 +376,8 @@ - - + + @@ -401,7 +400,7 @@ - + @@ -447,8 +446,8 @@ - - + + @@ -460,19 +459,17 @@ - + - - + - @@ -610,7 +607,7 @@ - + @@ -622,7 +619,7 @@ - + @@ -657,7 +654,7 @@ - + @@ -778,7 +775,7 @@ - + @@ -789,7 +786,7 @@ - + diff --git a/examples/bitcount/why3shapes.gz b/examples/bitcount/why3shapes.gz index 83faffaf65523fa520f9233dc6b012abca1e2e06..d7b0cbee8443fd468d91384eb18cdf2ae5920ccf 100644 GIT binary patch literal 8613 zcmV;WAzI!aiwFP!00000|LuKSk0Uv9?tA}=ezsvCE@Y4dc8oJP-ZBapcwY>?Hh2lH z8|dkt>C1TSUvH*Vl2TIYTAHd-6?=fGl$6N~#^s9$GDu?1kxERC(Kt>?g12Cz3BFd+ z5Z=d+pX&^M)6A>n$PeL z;N>;_yhGMWkAMF0>zDfQ>;KbL8xLPB|IT=3W_IY>@b|8DY~0@B`k%+&9j0es70%=m zLfp*H!km!y_in^tS&^~&W=zE4m&Z~zq$uN0!>{Z6@t64Pk54PMKU~b{e)+1#>~B9( zdu;QSuxeoaW^0!O{-v?ZtUmmdVMcfFh)qhi7(+^yefAQovrQ|DsU=H(AHRLmuirm@ z`FxbudRai5fSB} zBvB}%6IXI==}k#S5$TM`;xxg>5SE3?t-s#tkwB2ke&cscdec5RLSky`T`*ioj zthi7m&hOXyMH9-p`Pk1*$G?y0{bgxF=abir(T*TxO14^20T(w!p_+a52L`8)rtF&ohDTF&ndtM28@(9!>5S2ftFYqF9KG1+*Xg4dvKYNs z)BA!)FLuVk$L;OHf_*$J+-yjGY@nyZ=oXAZB%{JMCkq~BRKQ`APqeDiAjB_BPaxzIR6$cS0Ven4ShZucL=oC(` ze}0An$=%}GULe^EB;P=RH ze*qZZL`>P|dw2WQ=X>8e4)-|wJRFWG8t1s?kXmN07E?(v%X|&1FUBq_?|%FG4XB=EJZuG`h=cctN~|EndSKl2!x^%P8rv zSv_-q?%oAS&Sn5p)JAPOlc*HSo+Mi?(M>KWcs0E*nX-2P1(Ox7v4&VVR}-RyQv77^ z&wIy>GKR6DL`jvwTjwdLV$|X-2$uF~nlXXLOAD&VvWr!0xdu{o{pWnvDzr^T11 z#Rv3#Pg?w9^!=71tplSE9af$OR)8IaECxb!&H`ZdKsJ}$0{WH^$>DkO#|_}!Z{6LI z>Z&Hxk?Pq8@LmkBUkhBJqES!9m*S!2h>pAr<21%dVqaDZ{qvU}E1kJITAkh8wvlek zUfhxZF4LO3tC_*wWfN_8ckcvih$(R~5(5=Ol!7LskZZPJ@wvu6J8xb#ZwlsAghZf7 zErk)pyOLe0-YI$Wf`*1)0=tyB1|I^l!5jk{pSeYt#jubony1-yPA@xeUL$WR14GD- zL9sBG6dhy{MDbQiYJUAm(vYh-_M42XZdY@xRVv9Uu!QEqoEeTzu*gy)T1d5@Z14uR z#$Nne7cNmo*{EEiyLTp}s3w={99C&SLykSz%%awki7#t6`u!|_AzNLa#B!;St#WWS z1}KdlreI64Vggk%w{yPr@2d>}OhrX(?WZ2R320B2a|` zORTNSp|+sEHZS2)153ki;0%N(TH5!guOitN%z>qRPrZciBvGGE|K&^e{0m+s@}y@P zY-5An#)jKjG4hm08*H=9Y_skBg(Hi9Cnf2Nf7hX$*E1litpha$uW6`qDK&dc-arh| z8c;;clf%%jj0L5}TvMzPZE-DR1=lPrfkv*>(uV!Jn%{D#$q`B|l1M7G#8Aj;Dp{4d z1#UJ?Z{9t~{f0Z8!DVt)Ia_wQ+FUdS=Uk)~w;H{|DG!T(H_RdqK~YQO5F^X5ZJWpT z*GGIxM5H7RJ(P*Y9~^>cis-!U*N*RK8xoHMq=|UE^|K@qN~Y(Enq^<0aT3m zs;O#&V%6x$izL7Iz=*Za>1y%@)WjDg)!f{&1DlO7Ta7W3wTqH=tCA z0OE%Ka*Zv-&wOC=N%*3++pOYcNTg47}1q>5_!pEL{GJo$SWEi zdddw&UNvmS+OoiyU4|6dIZ&4q1WpEP#fWa-$r9b3x;=G!+O?-)KAb49t1e(gO@hOs z!cu%t7^;3BfAT~(y>5El^ma|pmJ&jVLh3wlv%O|^25NFOdNgioSNki6rq~(0 zCq0?s72)|)9#HYB@jMYofeaiR1j^tws4{zlM4Zz0Qs=9jTyfhmWuHIp^T%%%cY7Rt zCERt+C1uHwAX~}Sl$0t}r_Q0cjN_6&o`7B6wnRUc=-mo-{XvD`y^lZEg#3gqwC~3B zY=N3@+O@)w&E9P`Fc*DdZ+<8x@F?d@O z_V(g#%JKX;y`FSE`_=1=F6=7sL7I+e%(9K`=QmVl@L;1hS1!z)wkP10?_V}^&=P6y zyKq&Sip$w_X3>V9& z=U1CT*$p$y__V4QC=|OTl#L}lqa7yC*|=x%-wW>a&Vg8W@1%XFQC-WIQjR$U+djBJ ztQ>QJy~}|*_Xh6S6oFjh95`}Ps^O@Hs*Nc?l3+KZpU$v%YKC=~In+c=+kkvv=Y~O7 zS49$qNrnyT_D1=YeYVM1_JyspwkcT+)vH6TCAt*;j0KHvh`k}i#!*`nh6KbZaOfWvCdaLJoye5ZoIDbOr7T{1OycLl#%jl8?Sg%xftKHhD3r8ej5sR3_`F ztm|*r-)Gcc3f@1Tuaeo$*o}sqSb4(Idjt9Z9BUTp$TnB`%4Ct%bnF8iA@g7enR1u^Id0m-~)7&o1kZIxkQt9d#ZC zW;uB;EXuBAUo50#Du+@^H72d7D&N?D?MC^#z5%HNSQL6^yz2hjuL9ijkkkqpCB*00g&Ru+Q z^9CJLJEnF_eSV>IOns=ki;7rmGG1bhE+kP3Sp+;c(rY+rAFErMQ|oRojuKeam4N7zn$!1# zeTKcLHn$|~dr@7x#=Y-Fbx>paUR2!&zxchVUa(NQ4_^3SlWp+m!RD5+l$va`wS*wv zMCVGZNB8hOc{9la4zn)^d!)1M3&PIwlYK$h3j?Ot;39jP`bu47PMB(`RtjQESp@{a zdQRjrEAz&NgJwcO&9;J~j8$yyBG+3~PpYWd-@xNhW8UPph7MnDP_+fb?RQ*p)9>@$ z^H%(%^By;_asMIz&3j3hbTp^XJmoh>zHEoz6L)R*ciN+EYsSHzJYCl(efa@>JEt2* z-T4+-$JA%Sqc2+6)Sr3oyT*%^SGQ9>WFm-lQx^h(@^WO5dEMF~O?E2`9MW8iQ{#x__lW45j+E|^-5+S(kyn5ZcS!ZYPi3|oymQiDf zgwcaZM8#6ViXnOP! zRuxz5wFhguJ>8(*bbC74o~&YKN1s<)O~82iksGIE)d%-r>d5-)6s{xdD-&o(){~L77#~m#luEHm z5tBF-Ogtqub_n(C(n!LA!%?2kixD2g@NLgGZ>uE+*@0iNR~GRn_Uy zV@qDf>{`eDj{6<=JMMSfKNa^4mjofRPev;jHduv>8cG?8>?=vR?Fy0ZCAydBUZQ)6 z?j=qgEDtfG_ckHK&|E~KU=cVG8Kf#x*}(}#haHAH40jmrFx+AI)E%Y(g-U7vSHOZH zCm(H=B2leWv+o?l%j(A`52@);-l4ohd57{2<&T{twH2A2FHF9oG08(L#z~8_nUJ^l z@IRo#&$h+z-opX<7Q=mu;iKKy#pT0f9aEpa#c+=rZYFBDY>VMnD$pJ^oE$Y^@J6x= z#s;v42trh<5=A=|XvJ@L1%U;fZNDm;d3K3QdDI6-%=ukCNs)(n|x$_XDl z6>jw#ZraV3Yc(16G%}nKw(;n;ciQUR9_p+DS}F7#=HOxJ1H-{lvW02@%7a7BOsz7}gHN&O2x(jQ*{$>+W6k-26vP z;F6Z?*rGx$xl&Q}u1s!=*qM7Gb5l$%2!pM|aXz{6)Mw5KtALeY_*#3ocJ5DcUkn>4 zAm~Dr^Qx)BvhEIGbyBCz(_?6wTPKKO5&2PckWMd zpNm>=Vz$F7_FPR!3h2RA!>J`;b(;Hoxzm|E$>i)n6G>HWh+nFPgemyQ!77Ttv{SvY zpmaMEJSiT1vsru(nND=tgtjJ2L68;Ik*R?xo94%xcZgRz2d&%I%_~c{tut-Q1g?-M z#A?Zjs**9psd8zyMs?4T5?2j~yV2da7ImXLHx@*~RE1L+4geERNdx0tJuN_|BvV=Rlo;IS|!e;PViyD#4pd@U(<5Fyj>fJQF zK3f3YLHOo%u7mK~k#Gm$lRy}vFIA%^>j+Az*;8#GEb0lW*K*RT_$yY!Z?1vsBPCDk zMJ}#}f4ewyW1i&lYWTM+;_gaLb0rpPHVmn_;W$T9WaElv4$MIfEaUn7<;Thr4tWxo z|7(alf8fKXFMt1-XKUU+!HTRd-m|LY?@oY-(LLvLW%TeB*)nSN0<|Bu2q?)p>rwzH z(6ZXVl_AG$9Ser^lnWK!s0dmJ%h@I|q|VixU5q(aq9RJ{%2O0)b=mBZjbP-Q+W*l6 z%|ww>F-{G&wzCcLluH)gs0g6BW-8GdXCrtF$_X@!5#yV1RR4r^3vZOuA=H|KNhymZ z;{mB~aV0Sku%tZ|*!$VoS-qFl(ME*^EGgF5R9hRfOSTfKW!6~i*&`Rv7H{@+q6a(Y zIMm`p>qLMc)R5g42js~X)EaZzLod_lAsZ{?cA z$032#WTMsLlL1>tHB=j~rM<7Et=H1_YiVGj^*IIB?0iHZm$AJ+A_b!yEgeCR$FlJL zsw|`&oNX{@YPC6Q<6p4Wqr|K(OVanN)^~~C{t9O>)U}ai$q8L+CYr45ksHUFlpGdo z-v7roz_q4!NS%!+9lA0)1ZIww3t{EFDHld(x#77I(U=mwcQxQ)~jsB*;#jkP0 zb+$HsKhV7lKS%xj!`#Y-Pa7l5Q@1zGkf;Gzv6(801qGK)wMrgJAU9UXGg~gXx?IFM z4Ka~7UWH9yVK&K|#@0!lJKn|nv%8qARW3qI!6rw=mH|3)&Cyhnyq}Q6EuT$DXeL)$ z$`-&^=0HT*TdrPRDY+#Jd#rH!-5X?{Nl0z!yRT8XVguD$q=wX_?-(09)bdgT=ZgE` z%h!)9&3^Fw^~dKAOZ=Iw_p4hf`taT2di?u^Pv0MW+)O-fMvt%eiF)|^FEi7SYI(h3 zwyV+L`S-u9Kdfc~{xT4B_pap=Q3RXK_-4OV8yf=;4vM0QP*$Z<-y7#X|NWERf7aiB z#7`f;|IhtuEbw1{T2X!qPEA1Yit>Nm<271xx91EMOZibQ*?JtM$kG}zNJ>I{hoHm9yM?63J+F{q!8Tu1mYgad~ z8FpIVs1ev0K_|Q~sFkHc@P@CSD0vPM%)w92Q3i7m+Z`*fS@Bm%~JQZ}{z>u$g`YJNt4 z{duFsMP&WI`t{33pt930|8?IhNAY=suS1Qu?9?}5sd05!ww6r`&_gZE#bL0LY2x6J z$GptIFv?&;&c$i2Eu3!p0bGlQ91N~sb`eKLoPGq6CaHBXCoW{0hS%Z?#~g!e(Waym zIC6r-?=O`2HTuUkawy3J6s^v*$Sx$+*1hVgn1~aLK`yt7Q)Kl5c~n)*u+yRxpaO$g zREiXol5wgWHsih1K;~e7UpG6sMer?_Zzz+AZ5Cs(U_{T>E>DP`T87Q8ik zOw>{Uf)Yc?sbq)7i?50;BCq>`-$%v1j|+V-jC^v;q$ zaI2yH*{ zwsy|ZX8HXtKrV+hr=J{;fG+R2+YRN~d(FP5mp?5IENdUWef(c-zl=tp9!7Epbshlq z?wwOfTD>vWL~q)40y6~K!AmeU+5<7va>#L#k})Bt&=HjjlH-Az#4Y?r0%x_^tYk1$ z_t3G2h&2TVq;OOS3mHr_G21J^)o|d@aXzKvHIT8Q!z^*~RK2xUvyEge2Lt3L;-~Yh zauZ@sF~}_-xy%-K&w4t`5T~%@VN7dV0dUG71`eBJDlqxvh7K%85T=v>cUsGgrZXqw*LJS3U5-eLz;3#m*MeQ&q8FB&uzsywP zxBT&A{3Cw)SbiQZhs10#D#B) z#%fmkm*I;C>8}&u^`!S8=Z(B~{NzF+yQ3<&DTN7LgXP1^0Y#1+Yw$z4Eopn6B!Y=fhZ5Xiy=n!@VohQ; zPK%4y`-wh2MrkJiP)$|*T|`uT3*}~MzRRF5U38NBZX4VU_;@foZ59%X3J5TZAWFU;Hd83 zy3KpSsYh`Gvjm^G=&);{PcGJo4Ks>IH=NWt&D6C5 z-*;Z0%xi(jwH9wFn&Lp)|3Z}JwSrOdlJ|{Co&+%WT|STY3^i+ue620Eii(0H?=*_b zgj(yAEo^y)`!2X=5nO;2TRPBuIG}`Rswr9xvj&jjrfLQrlfmxe_cLX%Z(jU}MI{ew zS1`L|ye%mWwLHFMiX6;VImCehj%iMI^|)>ID4cVuEv9L4A{4Mb2s;;}6wOimwt9?5 z!@5GeMukwz*$)9OD`=tMg@Zr~ehWo3>yvB0|N7gJkYs&bU3ZkmLO7A_=gWv7PZkkn^htV(w280s9$;nK_|G zo89W>4G|EWCj)~sLo>7J_x$Sap`EjYV9ds`=HDoE0E$etP)(FZ0Q*)ra#-<;LHR7W>Utqtr;QMb?PIk+X%6xF%8? zYE@h6`#<8a4(0p%=19M4{H8m!T~ft&e-dq=6kCj6V=}e~)xxfk*ZjPJn%dWsvlc_~ z;sx(&?!i%Z#rcHBw7y5oUNtbd7HWpN6+oO~HuD9{$8E+wtaN?^WKHZvc7e~B+V1Ln zpYgDuWzouTb(zobi&ZO&W`?V?5bNfp({>?lR9nuZel_wzpO zF1GspKgLN|b9tjr__vK8apOn0dzYm~AWL2uY>VwP6&HyTGbhuc`*kgU{rctCfBzc) zrzH}@pZ4O7g;w*QmiG)l-n|>V?;~(~=BveEQav_3j;`r-5_QE^HJEMmuDxb%)??`|m%oe`y+6EUq|~_4tz}`+ rJ8LnD+Eg=&glyO}mev%YC~stQC``XB^qSyh zJqcuGR^?IKGrxXGDI~dE?z%!55sF|Iy5%9c(~Wj~X2!!9DSHr&PBHl`zJ8c29F4MG zl9Bh}<7fH!&-Z@~-@knL@$vKb@cH|HeF)z^#6K6X!1Z7ChXt%}S>WBf5UdRf3L|DK zxn6id$OgG+6w&V&|L47Y`TG9b_wqZ2AD>Ey|L;TioWrMYUu(0gm;SG$7Aky^)_j70 zf?i*%U-rm4>G97$e)}R1zy9yCY2)FG_2)t_Xkl8{+UH&E*s#6T^}h_iJ4{bw6)x;0 zgt!GS{F0FRc{kv&-H@^QW=O>0mxr8pq-ckKwO_aQt3tHEHla!7efajReEt6M z%jcuK)|c?Qih9L~_BrIW-s81C#A|(!*LsiF`Wbi~qcRb!D6eu!HmV%Gs}SG|DnkGh zyuQV5R;&pcO91bpPN|}r1(Ps>HYrF@FH5EFZ=2T$DZ2oQEHfvaQ?ih}FjC37(EH!N zeEXihe9j+_@cTL7`~Il>JA5CJf6=Z)Z&L^nf|PX6;wA+`R_K!uKYQ9f* zPt1x7RpR`9ZC^B@thQg!_MfZku%#;5NO;gfk>MzZ_(i8_xp*TMy=rP?pAcKw=} z@M~s3)P*2oMj&E-op_H>wQo#XKbFjaCtH%KYerB*wVHB)H5Lm}h=!G_VY3%O@2tH4{c9OVZ@1iE zOD=O1Z6mt`I_1I`h>Nl&a|k%q-}7GIS#f);&@m|wDb*yg0C-!onaYQnH7YQcAxvAr z&7$ONBsB|=kBv%i7cgS*5=$yBd2f{HWQ2@I0g03e{ciBwwc&MZgGUzU9Fzj80z*WP zIyl8f03AC!sSOP%x-z^zWhhZRp;i${TVph58v~b;0l+$MuIE6z*1RIE(K$t?=#x|0 z)ws*~2<^L|s!y>~WAG=Z?7IVoM^kn?(dQR8dNJ(N8KW0hVa3lJz1Zp3>7y5RHF~k7 z_XUq$?2UsD+uMf)^LSXe*^vC$Ku?F!5sX3sW}O)_=@?2ho_y4-jD(E7-~dLuy>xqd z^Y&s;)vSe+Nl=0^CaMx@{+eSf+1X$w!j7Y^=)Rj)H?3}3N{V1cBbk-Az)nF>0bC+m zy_AV3EjPJpIJuoP?>5|RxZCh?8)j!~A}*SXiV)Z}^EElEA~86~Q||G_XRjRvItp|Y zI0prC3LK2jHdvAB&vWnuHhU#Wf*Aek$L2a@bjawCaTa7`)+*O9!7B?<0VMP;vyT`J zgzQgW|NIOKB=;BB_63rCf#e%lAo+Ij{jvp;Zx`Q#VTe(qLyyLIQe>1@TtwTVk@4XE zhO<`BUjW885mWa0-u-^{`QEpV!#&PE4~J`L?Uf3QKnyu(u8BD!XR9q67Fw^o`~B;e zKg(Eji;MS#B}n|s=Cc%+*+h(ufEn_X8c0WU=U$A*= z^!Q_;p|!W?LJ|(>d1hs-wCpJ3KA6m~86L-GxP;AzVWl;?&ue%=yoM34VGBtc0@^l8 zb=a()xj%RBiWhdalAm=%H3v~`Iwb)c&tN3B`VPQW z%HtQt-Y8>S^w~udiYnr?P|OCbLX8=nF@dHT^GITElvlatTr3G9L80ihr?ym6a3qy&9x4q#14YHkS%n9@Qs zx-)xmO9Hq|YwoUQ26vZDwB6mk!&o?bZ_z4WG)drCk`x9NB;=5uYwWZ0=4JDyXkqWN zQOYP&lyTKTc{W;W7c*OaK|{kYfnC;W?^B)%-LB>opIKAz5<)SEAy`6BZ6?YEjFS7w z25+!5_Uhku;gU*dcUCU70}iNSjMuDGvB_!W06(f}yg|)YA zT+k+Y?M&35AO?csQ^IsR=Nz2U+ZdfkpQDaetRb6KzO39eLsB{$yhK4w(>po7QT~2eLDS@Z`tD)yi4Rs&omfg zgBfGP?d%wN%A*a&Y@;#T&fhq)`gc;2zWR3^%Jp^zWK*w+t+YDMv8D+TjWZ!h0YK*+ z+3LFI&OCTUEHI*5!78yeVr8P5l%`C9TJ@@u*rnO3=C|BwBmpV53SYZ`H6>TZx>n!c z)F7^~n=annfa5sNY&6#X$iKV0gD+R zbI_QIvRFZ31`lr6lRQGg9K^2u4Qsk+VCZ4F`$n%a7?N%6h>dGRIA0xU_C6SjrM)Xvb zL|)PG&{Gx^dDXC)6Ear^3~keTA<;$`@UG+lDJ2u;PL}BQ)a|L;)5KU~HVQp?4WMGR zEr}(FqJn}o+ExAvCr@!#ODZ({J5i;XJA%=LfO_>u@Jt!hT8qYgz5u7kQtczSt3 z>2A~Arn^n=+q9s|9I~xxyms0LZ@mY|7Lran(9}s4FD@JIsL)ZNqrz3k`mFP%5J8j- z#>Bu{h%p#d5S8$&8|&*3(jlZn$W`Z{e9D|bQK(6|lTs50F9r)GpIPZM*0ewCNfv#X zYhUL25}^D^Po{W9c>a_JRJ>|Dw_FlND}pJi(rTou5K(+`Kqd z5Krhr{ccFl2-LW0*9J#+d$-%fV7J=z!sxV`fFs|( zZswpRs@ca+h31CFH85U5bGzD2iR~U|>UXCd>hVmdX-B9zx!9RbE!4OZB3vL8bCFP5 zYO=u9HtOZou2A;F3>uzR^#X-rMnc)y(le+qc~0S;)qgLz(|ZSE-Ms^+5L3`Gxq>cu zVJH%^5jGT}o-Ci$xwqzCaumdHY2~!ML39jJ5f-+Zsi?Rc{d9)C6Rd0jjm|m^m_tc5 zbOaMAn3zeX8P?S8t@2AOXEq`!1!D<~VP~`}&LtsZC(ng>?1siS#9mi4LDt16=eSTV z#b|L^fK==A*>xz-?%5mVd*JL{Ro^yT*FKQQD<+G&IAd&{_ByX1keV+nJ{Lp1;NgHC z1w5dLC8e|j(WFTU=$uV3U<**g)@&;%47NCt0_3FTVQ5QM3cQz}xuLkLdsp`-R(Hw@kX!Xru(5Cr zHGGiZl*5v9{r<_amTm{#4xV#xB-OmpfsZD)s$Rm{SXA{o70(vk%rfAeDHAv5#-27D znyPbS?LKd&&h4o3(J8AvT3^CE-JlPrOw(PZ%h#Nw+oAu2Il2KwM>J(}iq7q-N}HkE zws;d0bQM6`q+-L;c5%||+zSTNS1_n_Y|6BIxLfsbKDbDtoS0UlkF_&wL(SEF_BHbJ zc~qUDBS}Y+jwBsPriMs#w&YDLF-hA%8^B@#Nflu{)oA&^u^IF6%Y8?kXP0$HofjyS zjyezPV>}}!?N~wa&QMX#V6N7eq9Py50n|A=@!CH=qyyJWwvi58FHk5QxYp~g+VVZl zfSSnH;7O?nwlOxhH1qC@f4 zOr5*<;^qxHrglv2nEL!e>6p60)WV)KBYU46Xah;acxi_iakAdbO<>>doN@=?4!|9N zpI;~)fFE{0Miol%$`W&OZ8slR!d!7BqClRS6*;>8r(;~lxQ=npFO-gP537YyYJkZZ zOb|4|deRC|saQ~n$9%U>hMdnzN58#7B#UTlz zL1b&G)gV;6_48;#L20a@Xoo7cb&=Z=)srep^9?*6HI_||HMD)XL)8d~>+iVXCeQiq zWh*@CyoU|!+<(Y_>sb;e9nC2;Px;M(FWcky#9ib5PJ6VmW*qFv({+8)mmko#bGmWV zosY;mraluMebvIQ{w#CfEnaNAx|#AJ6G5z-ve45jqPt7%bLlo}vbFLd?P_-@%Iz_y zem5ZMbwRNkL9v?(3e0p+Fd_aikP#zL=5pmrosI}9ky zHlUzoZ}nJ~ua+-nd-TRC(7Jo4ol;7~2&R&#pyeP+oH86yn9W?V&d%Ty8BFB06rH3H zi6EIIR#^!~k;=}Q-Jq`X^c0?=a@q?Q3_z&C1jA^e6yfZZvwD)JO=&wz=U5t&4KaH3 z7IQI{bc{KBolVXp+DsPheQYi2E`gy0phAPvf;9(BB`ZOewrIHI3d_!`$zuIKtz2~% z%}_M#$(aJw#!NF~bS?pSEZRf;6J~1iozImnfm!2VfMB9>(MHmegDM7ceWNm{*vy<{ z@d^U_10yN3QT;0&G3!C+$>x#?5S@=k1Zq%3TC=HyVNO9x(li@%b_=;>P3RVKvW55> zW+_e>1+*xgk$gLUrKFTqbZn(i8tm*c2gL>2L>5QSb5Q8I=i>+CbBi1%R%Iuk}MR&qM3}_dd zMIaY0-r=zYox65tcLC1v^(%V>zmSzXhsgPP{l4z9otdWRSM3alI;J+$i*|UVH*L+% zrqSD2veOW|tutCK@Mu>jt=M^`@cjw~_Kz*W>i)R<<4J#99dW^6eTX($Ru&YKc0Qmo zDUu4KViY4?LuxvdcPQ^r-l4oh`6Hp+OJ*iRoSC$V z-hz@u+ z`#?Z<>6f^48$*fK>mu4a=M;b~I$DvUHKSGQ>WRO9{qkp-QQ;w6>yuU1wi9%h`dUA$ zwx$|Us3|9W@Km_XZ@6nWBiBj^W*TW{gzY>!_D-YTJ&vv^2$=|q5>8>r8HYWM8n}j6 zST?%vFcS{xdTS?fA3PKX%Zw1{COV%Rzmv+N*E82wvg z*WEkgBI)`cMT^lVFoK{t#vo!Nw_{-^3cGjap2l3yf>9+-L87UtwqS_LW42CfRRFJ5 z!?kmNQni&x8}i688Su8oN){oOU{xtm!lY_nmHaN2DY4Y>6rxB7Sl?N^bs?~G!HL2o zwp{HnkIwxm?kf+hG5gRy9cFTwbks>%FXVaVl$%-ZbS6(RnMFlTm91>8XEKpXG}DSpl#VmOlj6}go5lB#=`_>H88a5WET!hbS8TG;i7TXxwhq$uLZ)t8H?Az* zw$6>bGN?o6X2k<7;WB$A@D)r&>1 zAcq=nN478%a9@({blbXdW$Ctcrfn4!EqJk1BSQ{>t#_UydMc(J6*@D*b0C@RCUoOE z(M{;wLDFIaSQR|DY@>3ydL;~iNDf@YcyKF!pX0s2_%E8{J!Jf|^Sf`?_-|||?br-{ zhxZQem%+PBwqyq2NZylyU;?sI4oG|iE7J>wI=psx?eO}RCEVflw80$@Ik`ln#bE{? z979H@ts`%u_0#bBYyor!;hWdF4#ICo!X1Q90%7r4v$hu4Ab90M4RwnT?2W52Z_y|1 ziofD&_}x8leWc`Ry~xF@;omOK+?Xf1d^P;r6>)bZC%KZgQdkiN>vGU6+Nu=DPzfLr zmAG|0pT7LqSi&Js0?U6DahDH#`1Iu;AJbyX`zP3u)x~?(D*3w;AYyRO`CJ)1d_}el zTD?H+@7|#pcA_~eicnni1w?1>bWSQdnOUUJMQ}wC*huKXk;j}gR<5)1La0jc7Hsh^ zVz{^FRK5 ztiZJ|>z~$2zQ8>-uXhdXpi%hGFJIf8RadJ1e#jq1+Mf&k$L7)c{ouyR@c;YuM_IT0 zmxUhWR?A`>x<${y=0c^KaN?lbhPn)#V-4HDAlTulusg3+v#(X7*Q)VrRefz?)5t-g z95qC5L!`=Y2sLyp#qeSDcq|L=ugXHB6-f@LyhSovDhL*gfFT-_ntR{0zEAY{D_lTr zFx1rDmP|FBQ7Jo*S~3`46Zy0(diI}VfU8aIk-8XA+PX401ZIhrD`BPjKB~CubMe0I zR7xe;lnJYnmq_Ar*o+)}E5C=YVaIjWHvTx!y#&96^2djzm9@WiMwq8=zk8Q;O(f74 zgrEd0xmZ2Ahs2bU259 z$qtOoRuOV=x`9A7Bja?X!)07+;8JlveEIruquCFhUw(Z4u*RRowqD&@(c5>c>*4Pg zK7D`iahiCX29Iy+L_K`|>w+p$t*>{?b~75h{QlSNADfwgzchlX1*6x(COKcDFQArN zcxGAd-xXWRnt$Ib=RW`AQ@Q_K{`e6-ef<94_nWc6fBWl(@>6hX0)jV`|JyES#$j05 z!Y?h%!fwrLbmIoz^y&4e)P4iYU%>{gx8wQ&0B_@);CoNtc*}6yu@#Ao@U@t(W|QVW}!}yzS5hU zPtpLz3*{I31RYRrbMvSd6_dPk)dN$_9&3QtP*FoszS>wOjy1u#p50WhXG741tLa9Q zOR3gtf;L4Jg9XTKg39>khw^9nybSqK(CG~%V_S+`>fxWq`!BmslZPm~1@|JVXW5H2r*7FEh$K9(%Htp&pDv(y8^Xjp7wI*abNI%e0i@j@z zylSakt;d>Amd84_ZY?aYHcZ)t(E5`eYv&Se*5B^~c z|Fk-=tp4%sr{> z${-qt>6i*kKDna<>k))0CBQuwy3qnO12w3BoS+9$h2o0IUQ#R;FjuMkALC2Sbi_agV9i)uqR{Hw)tVfqgIuC5sA%$pz3xGx?gKZe{|*xAgI2_%nR^n15-PEiqe7`7GB6tkdLA z;oJB4@%uK8ADYKDU7R-|{p-dE^mHpVeH%r@dOvSW8h2)G&0v$s@{xMO?r7&$N`t|K zVcw2&7z#0&(+a?wRwi6(0;=EfvX0+{t^sE&O9-)?;2G|_;GQLg(aIMSC@ap9 zf`dTb)?`MBDF)TC;OE>7c8=fAl)=7v@tYDj`hsQ|78G)+qAA!Sq1tZNFd7e>AK;kg zWLJ;dR*$HhCrQBoyA)gW-?lm>UvWY!Np_?j!_ly=5U)`ooJXg%18VV@sg6BJGLm9s zK&_0~tg`;?_m4}~9b0a@9HT$JN|hc4^EYc>+eE>`I;=})L6>d(vQOoi9G6!YNkG#=n}uEpa(VSY%>79s(7e!oK_{%y)^2n2jtCT-Cj-I-sRgb2y}Y`6 zXy+^;5G}|oXw~oK)vDhL&XNMT1@VGb3cS49QgcqPOvQFwnAH^3@@h@a1`v1udiea; z<>c1pkMozx4Zj_1_G`OQe4&&Tu-617WALV04;dtE8&jOT|1-3GDBs`blD?Mkt?bcu z$tu44lW3DrQUHpHRd%FRO{^Gl3C430!(npPqAgy$;9afGg3}TST2alobQW3HS2R!PzFn zJ}gXV#fU@7##&7d+d_B|AH89dd<^mZvQPV)t^WAWVG>qd-rz6%`_7NJ^CR57OR++- z)wyPTu@qD;XRe=x+HAIMW321m%GWQy{m0kv-!+kFAN9pM8?BZoGZIHbYN$b4fAN7g*Z_5VO?d^7Q^UC#mS}BF)PKAVfG;DrbW>@2%7lZPJ zyehph+{4?R`!>16VO=btetiDYc4G`^*rrf>EzCaEQoHuq_Ik`ezSpPKCjD(^X4~Iu zw1S1rY_-!dlq?)=_7)pTxGEZ3^6tKknh0(sjSo9G*1uO0;$XGqHgRmP$0ebI^_S~( zvPMX4Gyy6~A(6AzLB<$rVwo!`I$ATPV3dmfF-PDiVFhQCO%BjVs7i-5RjrXCwBiD> z_8i}@%z7x@_4b$HruT=J43rvoy0uC Q?e4Vs|7=;?jHu}W09_IsZ2$lO diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml index 858ec7e0f..3ae4595f1 100644 --- a/examples/bitvector_examples/why3session.xml +++ b/examples/bitvector_examples/why3session.xml @@ -7,7 +7,7 @@ - + @@ -103,7 +103,7 @@ - + @@ -172,7 +172,7 @@ - + @@ -199,7 +199,7 @@ - + @@ -247,7 +247,7 @@ - + diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz index 9b3c46d15aa413c0ae14ccaa2c5222b58c3db809..055bbb4cb2554e450de89e69804015d87336152b 100644 GIT binary patch literal 3023 zcmV;=3o!H_iwFP!00000|J7PsYaGiFe&1iAw>*SERo|)`>;odOU@&<}*jLe)YFk7{ zN+kKjh+AVmW05k|Lv}%*k&4R9<;QOax+mGGJ|K|ylbym|0MQ5 z{XcEo)-D`P^fi4f8FH!HvD>c++9pM z(D(KBhbFD2CEEV1*W=Q9MX6|NLe_@Ds+@f3idxiLPp<2z#IrsEjFXi--Yi zyieOy^^sMi7Yp&UW%(Wxtw}y=PdbsGUfM~f3^j$X{d_-iDAHIG?J?>NMdQ6 zgwES=b7;H)s75%_Che|R<4mimQVA}i=LXJv3bftW=FnW*P+>vDdA!sK4q%^9ta=JI zXs__{1oUrxd^n1i!DvTrUa!0_p?Oj-jD91;24*u=ase0MSgw!@dSs`ET{Z;Uiz95H zAO>J(!Y8yYplMZbi1FQ73LIJ;HdgD|q2sn*u#c!NxI*5FQ-D<+F?Qm2CLU5$r_1Z@ zCG9WQE5oELLq`>#G)P4rh~l59g^CuiU!Kpv{^bX_QK)0D)xkE}lOn8oD6tmOB2^9} z4B@n|(SW>ry2Hn<6OJpleF>TIYEWQ&alh4Zb*t3Y!GlIl5?Yp*tSW?Z;ZhNg_mQZ* zaMDwa?hd=gIc*-{rDwgl(|(wzv8SG>v|=q2$Eeyv>spFuHPX_h?azhXT@dzo`{nDQ zGzvyN!D%cgS%s_-A8lwN=uhZVSEC{JLFP98dKNIa+`5i8_Qi^Je|bIg^SJ8w_stFl z0Q(TwI0RLDaz zlHhd~P_#ZOG!zgwR+8)aZ64Q`$>fLF>dEc?yul$x~7%`I! zB^y~bun|Ca5EZ9UN;GQP1aIEb7A1D?4MmTvb(DOn&IH>cqZk*DkQ(9b+Ztp*nL%m< z7FZ-O`fc--z+{?Q(XNvK_r_LfHOH+?m$8&3D9uIEP_6 zRvV2qP*kn@gf{6xReT&ZzEysu(>8L1_R@Vs6geNo^(*in<0KC0QJD029_Ez`d~#2MMj=?OF;F zH%bJ9!5m7kMXa3ccy{r~|MiYs4Ej^+ArgfE3Tl$^H5bY~33zVb>-PAxZLsgzpTTpp zw+@3Wm;l2fV5+7$2I)lej64&)ZMW~*uAKw1LbzvJHRgZ}O*tkqjX7H|`@Qh;4}MFJ zzFyRx9Ak*8LD|*_b!@DldmTZDz%Cr^Oo>07qYv+)12vdD=9CeeKBgW~v&pMh&n5BMg-!Upm@6z)iel)#XL1-_qVsSTY7>GIt}(W_Nh!Ni>O5W8Y4#J00c6df zw%B3sRxKJ;N7L;X(p12n&DAcsAMW*OW&wiEy=J6L#S{mk**Q^8F@xt~+(DB2tMO=K zIy9M%I6m!E7^WQIqA2ZZ5}cE|^||H-- zu&-9Fy*hW+LR%Bqnp`yjbrDR)hZ=^n8MYR|8QdB9mA*6We$F1@02bs3B__s%tw;>w zF%wpA14bx^;dujl*whvr~i&|ewOFqs^o+T!y<3LHHyk7=! zpLZ93LLr;^{zaytZH1rU3>^iNndKw830;WTUp@|Xa$BEwN}AbmbKF(WnVjReG`zkZ z-^QYO^=)&krI~3-$Iu5?L$Pk1+i*Bmqmm1tB?cph!_?tJ(h#S!ll$kdM>K2=BBr1B zbM2P04Bc{tHt1kY6KV>jcWlMwl$x$`cgq4 zs~L{-9LBlaTPhg3UI7k!ZOYja5%qi2l9)K+sWl9t$FhkVW?Gf5bg3?@*u zV6J!<+v$|dK&W$QJk3pjvC~|02GmZdtAHp2@yQ$XN37Lb^tDw^q z0Omn$7;XR^L36nx*bu{2hCx+{XP_pXl%6x-CRJHEp9sTvHjPX+h(VN*(eg^+dGqezG*u-}-YYvQw( z?u&O+XTWTi0At4Tm@K2LP}iWRHQI+Er`W~_IV%awxTM--2EE8{a9a=&1Ls*#+ZKmI zIvx%gJ5qcYCq+>`Yg2!<1kZvnVJu6Y#8Lt8PSOPlmLu{@Q>?|hx(tbyMF0Cm{5wYZ zJ4W{MXzuEpl{DNXyrEg}J!SJkJQYGv-u0RVNIq8$#IZN_ls<1#E$ znGDh&xrYXeVYxVLHdllQ%-7VVJp7r$GB8HgJNa=f`I-8mwcF4=qhFI^XjU&^17zzU z&WB}DKYXpriH8F`9ln~Q+A<@mBx@`%U&~pHp}q`ks1r8YRZhr1eA2*ht>?W)x`4$UEa<@Gi)WsS&YC>-KWX|X}099v_ ROF{7N>Oa7i;M6uJ005=W$6Npa literal 3032 zcmV;}3n%m+iwFP!00000|J7MtZyP(3eb=w>+dK>ws1LG80=WYi3m6Cx?8^@H8t^mM z7+-tVcJ2oI>-V%Qb+=^MR|zsR7$dROP4!{1SXJi~n}xLdn*Au$tY-Y{F~(Gb6SdT? zw*PrG9v-ire!U&fpKqT&x7*+I?ftm@cJ)hse)#Fhg+F8RNq*m6m~;aDnC8-$LHIJ`+uMj#RhpF1Gb`#;HnO9Ee1)=6eIH5h_{{f z@gHbscER-$OO1^){&a0EW@%cxB~5(BS(k*s$A9grEW}_=O76kO+}+^hoKtITu5h<^ zy#FfpKmI!{T&(q298ne`m--k;`^Zuga==2JCJ4<7yR-}2pEF8}*E-?!<{ z!{h#9v4Otb?0#smY8j&4&&|y|gaqs|*pknqnkrfB>}vDfQ(~1c8}Zzqp11k&Hs3$z zuXpg&me;=7yMniL^D%$@(s!Re&A!_7Y}%_Uqxx8kGo>EH53}4VCdVe{);>S{-XC9( zU#6JA=KD1HZ1^CdRu1Y#s}h%#Bx!S=*+%JC^OnLf_Ycprf400h4EN!%{RewgCp_HG# zmIZd%FRZ&794Uf?AEQMxuZ@R?%?=)Z1q+-tEM_?eTZ~fV7PZ1`F3iJFl4COu>>OYF z^}c@rz%e+YiG2v>Q&w|{lp9qa3My)HIgQrNdGg!h%5SUvnS98tTkZHw3*ydlyeB z+Lz1g-6b6^QQVk12XdhWpSp#LJO~~CLsyunfc^4(2KK-H05=92SZj6gO&_TvtcI0X z3-uCeIF2xc)1gKK^6u#lA9tH@TDkQlWag{Mfce40Qs>c~QM(PEEOH?=i9Y1s1EE~F zRD#FzNYqg{_16~N9ka$cYaX#n&;9dVAIEtb2NV;PR#cfd#@>gu(M$2%CA9R`^4F8y zy)oJ2?U!GVXCo630XB^TN>(8df{&o45V9MM{MGD;Ly)k- zZ z;Mp29YN{>;14pG!GF+tCS01Q;M|xM z{~Xte54DCat*PaJ#<#F!x1i~dvG0f}frg5A5^_ZyR9BLRb3->|-D(2&gFFn@gYfR+ z)#r|e4edH71qajANQXHKo*wz1&d3Udjk-uhjLW3v3+g~c>tG$dO`j{|L*=(tS;i!4YH=>06rx&{63@(E=^NAj=j;&xAqVaX-c8h!=6r@cXHO0zx3yA*dA!|&qwze_t)3DosYIYY~$9g?b*hgqf7Vd zSZhC3dSj||GF4ipnjhI(<)c~B&2n=50?#{k*kj`21&nDy!_Bwgm~LL3M881Emh}z8 zF>q`->uR$3sV(#AYcoC?+%D=h3MWvbT`X!7%2Sd#U;GP35I5N^gC28kCd4x1xgmTi*4j-t{YA_*2u^zm5o7FW(L@wt}%&Fg82#!!Of1>|`A` zZv+Yq3U93>oUSCSObGSFkKtq?K#uE$!~@DICpn&?#ML@*ZEsrrR$B6DUh*n2Ih_Vd zn&bN=XtLJK- z)3_AAxt^cKpuGFEoLVU>E9n&a=!z!EN{PJ>ih3Wb_yAo34d1~Z&`d1L*~$I$uO~9> z212ZVI`p+W$uhC!hI>lT@41UBt%eAGcg2GtDNSd{?_v7<*T=8@@D^bQH;>sy(8Gq9 ziqxiDz%t0CjE@W^E}_voz;>|qJaW?{g*pU9^C@bsEkGrqC$HdBm3D#2`7CfjUzsB` zhI$joP&A!TfeEaf%BXIua zSj`YV(C)5hi0GjXH(KmAi&wzt($|~;)dh8vhHqMesA@8z?ipdyoeyCk2wPi&(z~Eb z7qICOt-Vs6UYYXr{$fOQU$sJ5Df-c{0+sZt^qc_~#PMcK5?2wpDfbb3!B5OI5>e?= z<9huPFG7uonvHkp?ptpO>Q^X2@ST6x)Y?U~PVUvR-Z_@!%T+hu9%_5O;_=*9oxR ze94!E0{TAjNQT8FiA!g^@ zsGz!m%}wG_I4(m&>`Sn)X$2vM+A;|Ui(z_cSgAxO9CU=@E<;23Pg-Q-JQBT`BX5Pw zMk#PXeNVne%c(>oO9QKq*OqYlT&64 - + @@ -5820,7 +5820,7 @@ - + @@ -5828,7 +5828,7 @@ - + @@ -6272,7 +6272,7 @@ - + @@ -6304,7 +6304,7 @@ - + diff --git a/examples/bitwalker/why3shapes.gz b/examples/bitwalker/why3shapes.gz index af9c6fb59608d99586e57fee6997e510a92ecf52..fad0fcd7395d1b72bac314121d03e90a60c992e4 100644 GIT binary patch literal 9003 zcmV+`Bh=g4-iy(ufG|DlsXGAG&%1(jKY_p`q z$_0Gqu0Q4Lzux`iK7IY~o!G(f^Jo9(PPnf(|L6Lj?k4|y{psrtuI?WE`woJZ@9+Qm zDU^3U{4I+N(K;ubQ%E{NPC3TFJ_zRpr`2ly?{DtcUz-(~Sv^`f;GBRA2o-~|Nl2l| zVh&)*z1#icUB3DJZYcfRuU~)voWy+zrJ|p|4K;}S-`sERuRq4nH1KzpT(Oe#3%OL>xD zQsO1OyxQ6(QV@b=5uNs~^sd;ZRGA%VppZSj`~Bw2*KqSGUhmuW_!_->zP=X8C*_Lr zqzggsy?UvA^%)~23qoiu&;+R*8o^+rCJc(-QeP324oPQ+0Lljn z5M=47aX~p>KzP#E(|WN@GSAl6tOI!uj-4VDK12fwty7FCxfJbN>T3btf{h$>^2Q{H z$xH18sfamdG6%}}{pOeSvzGq)YiYtg-R*Escy#P4)ihF*BJJcIIm)a5I=nAe-~9Vd zPRUq)xEfbJ2!!s)yp{w_8c;pAQxh*>r>Z8YX)zx@y#L3%P7oU_y?<~AQ|F_6Qq>DE ztN5ey|N8mnbCH>K|L^m+)My26Z3W)fNwZc^-3n^A!hMS6h4Ra%o3EucAKb5B(hfhC zAHNP|nY*(1pq+y@O@NR0oQkjKbka^F zVVc#?v_j`8lh%|;V`W}Fe&1ab5HezM?@N#(rAyw65>-eG62YXl=uaIea;@991BGfH zdK7%&CM_tbmDA5T>A}aj9s3gZolxeyZB8+3%-Wu!+j3b|HvZ zA`UNo2nKPO9I)9s`Q#&d>lur01Co4ka&!p< zOj|yyQTZcuS5CV-*1-AQ4N6i#@XnS9A^14V4i_F5C3sbkkJI13r}WFurj7Wbu74Q& z`|0=F8Ts8|0PMe+&Qo09j`}^lA3Agg6L&oo_lO{iH1@MF4^-P2>5mf+(`+o`6fkft z9>((k1J?kfK=Yw%eC!&pb&V&nuxS~`Xrbizd2#=oi_8{`L@P;JCD@2;lm)9puwf}a zKCKq*lmf4<28_bn5~>!kl4Jt;EQNx0;I`iFt4kUr&@;QztZ0glD|E=2B%53YO7J@P zZBg`-o50m`$fA%(v4E(JVHX|9;{Bt56pNPt&JL5cj}cXG8*a<|{5E7wMjC4wK&eQ| z7q2XsOogLJS)ClM0rYo3*Yn-6uI@qItdjMV%P5MP6H@f(rBcSaXuXZ?b;}Ew_%hp+ zN|Ta+-bJAb`jbF{oSe^Do22Kq={|pU|5LZx{WF!Kj#JH5+x9+>`T5J&&&mDfe*5L! z{^k8r|3N?RXU&xh%{}^{JKl+rLt1ovm|kwoIJIhiQc~toZ2Ft17u?vnYd9Pz(e-fi+o+$mR z@7FEIpirUKI+2j*%h(N^wM;1)9Z_8({gW*A>h;JhT1viPab#lYbL;1+&LWco(|ow zx*pF%_gsKo5*eQ%aS7Tos030vwB=9RM)!w#{HkmErD-}O6lh&e$|og#6b=Z$1RIHC z*3;yj$8-PYed%WNddwzkb^#IuG|_8SqMl)fB}o@qtHH0T!iVeY+H7`q$nn_+w^eel z7|k>v1C{d4hxgOhp*F8-EnxifKMtjcx;&@?-Jz)YwD&%{7!EVtr8z4FRx&$8G(YX^ zNPYjgwE*|+pXC#?Gvh9U+JT*k%r1(|ewe+FGm+ywp00#3&b7v=5{42l(E^UNfK4r| zHm|(%q1AcQ)@Sv=aYnzC0{me<#(-ySuZqjp3!K(*Jzl&Xfk|n zN7V|>M1O}`Zr4Mgy*NY@Ly$YfyK#wF0T|-?>qYB0U0p)_a8zpbPPGP734>1T)8Xdz~onqQCvDPthUdQU!hKVIp&#K*Nm}V$K zODKdi18$VF*XIkl(2(!mIOM!MbqNHi5d^6dA*g6lwGikb05aoV?0I5`dL|gXC|BJq zfoCPmQ$P=`-@h}KE;maxmk8L51l$zN15GS%HDo+V9B+wv!F&4tS+U0i0XZ^ev^$zn zG%b2XG$rKW{Ywa$MubdDZV_GP7U7wG(Z^er-@kS6%^g3k6ZsdqD; z;ewM;oP*QRwcFHV*i=lEU1q05#;kO5+Cnyk6_t@uaM+e2@~Hm7 zA(-kqJx{0F3_En3wN`>P(ga0`b;v1jw2s2NUvF-He|P=qPxtw{jO_B;_19;2HkXqk zx-q>ZV^U~93Q*n%j7*q~2*qJw2!cJzxMECIK=rf?GP8wAG-Vo-UENCGl9eW9vQNzH zr6EaD3T?erQpCtoLf&en6CcSuU|9=JOt-SPX=OvENzABnbizyEn39cI6jT&B2^8mA z*^(#TE$XdX6j&~vnusd-TzJ*c@J|%Q#K3X!<4&EMICtXvYH8;C@+HgZ>oBverI~Ml zd3kur5-5(AK&vd;jWgeX=goZgQT({5Xn>0p!0Bg0p{XV zpk3Xm`IwnK^Nh(c^qiU5)8VPZQ-`Nl3{PZI6d{su1(sNt=w)5QM$#1jaH9hLQDPHoCaYGjFGpPfpDRycM# zjyi(bSx045d}sh;2l1B!;%bJ%Y7xZM9CT+{*X5JVAg<@-@g*S6BM@&KxbzT+a|iJb z;&TwUQack!THF&+$rsaQ`#)C4i+=(z|1MAanitcN}C=%V25)CF4#jVMtexB zuQpOzb#g(cv`%Tq6xJj;BT6NFQV2>BAhTe{fdwSBfzs~4mA-4-Kk#F9hDGPgN8(F! z0MnW;&HC#zq#Y2^biRDye0j;yI`-6)bsjia$9~syb(W6R>3sR4^QFtf!H!|r8ZXqa zQYv#chAHJlDv>^sFHe~?sm@ut3qU&Eb-L?x*Xgd)U8lRJp*yXWOF|{kHgXnbxY}5W zXtdGf^L!uesdTqE;5xZ=a_i*Q$*q%HC%2~}w=6SrNJ*4PPEd3~14I>K28sbA+>+Zp zwZ#;Q@qS6SXA|q=!0rUq7w0-b^~Jd(Q=UvveQ~Z6RBLfgdYO%|!3wJoGnciT*qsvLP^yA~@X1A&8`>WWem#MaH zyLdiKXdI`dYs{BR)G_$X5Ms3GonvW~4N0hwvIr@P_D;u#I&`(Q`bh4w>7BZf}?@K2g2N zTee<3`lplYC3lmX&<3f{!X50B`fne-|5hDkdiZE`tz=#1y&Toy62}i8-v47-cnL-} zH)J2U+nDX(VH6MpTe)D;7H^qMR&+0otNN|+WZJ;q}+hmJ=vu$$H zwp#!yzkIs+dWatf7xE61Y_&phFa!HI?$-Pq?4zaWTcqLL>{`I))2AR!^;#qH34G`p zAG^kDUE5!qdZ&Yl*VUSnFQWgOQ9^?YA#%()V#+=icf2?#QBo?Xv*dFvl~-6^JAuH3 z1^Y$z%3XE6zfoPNZTm+Z?ZB;JXIyYp=Dq zu~O^R(+R-r?`tj2rcc@m!V+mY7Q(X9AXWRw)|1DLTI>7mxRFO8yeR=^8#8e(PCbyy zYzzof#tfoJ)(IC^*>J!!bEwkJ5!6-yYMc0JThM;!?@z^x89@Gkp1N??OjP=D{Inm~ z3K(*5Qsg*X$6SIvEjrqSR&o7)$gWN10`@p@az+3YYT&rV@?rlj@cyl z++%y>8jY-B?<93|cv^D^(dm#v8PCa>=&emPAB6KBhku2*V~F$H_A&0Eiiyg#gBBM3$5jg=Rl5Bq*z?T0)kMYKSxfH3|bgF zZsv*7zxsaNQpRSROt#VvQA{+-3wDlz<>(7RULyUIEcWX4$P5#am5$LV8A~Kc-g*=Y zm1mtCi3L;GgbJs2>#fRIDC>Uum6Hd6u+D)~U(du{g1{6^vaaw!W77u8pcebsgP(sU}60%pY~WkzdA0_UJG zxtPd$k`Ii{r*Ix&>^ws4JVL9CI$3b)JVI;ZMK{G4X^I3ClVN8|3?LCr4w;yAanc-U zC6?pTmmO+Vg};JOtB;n~Fp%`{H zl=dMEp>AKbEH~_sZERJ+`92JLEY{xc_87MMP9d%R{3-iA>i6aigR`>amTf_eY+>V` zVpY{V6wx%$K|!jTug10gGxlm;Uh}!OX{kkPUn^^&>qj^^JXx=@PRc(#t;fZU@^aO( z0`wG^v33=(+PtJI8R=!2>ks3uXHwp|vg&XL&>j2ym4b%y_V zq*}JR#-*A^@r_62R5F})<5*Yu=416|agI~bYSq{U{mbq8mkaurr|VzV`ln~n|3$TI z*FQay{%Jw~w5Wfo^bb?%>_)CgV~S+0iHAMdTl|U_y9fLD#DiO~y%Qqj3>aiWN|2;P zPJzE$N! zA}Or&7)8(whBaHzKD(UEuxY8OoHJmFE0uNiJ(~KmXULhI^D%+6-bCf3G{`CzD);R( zpPrD#Dm7zQ^P{O*%VfZDlnMZ(VHZpqHV|5otoLXiNzGebqJqp_xsM0IAY&oKsDfk@ zNm#`;p$(2j!Dh3P@m;y&+b0MX<_FfM2im@Pb)ZnUh)1=Elqu=#b4XG}HpO4ksFI6X zX_ZLEi#(jZrjL`G|kRE{l5ue29QYa-!OG9k2cV;;|m>Kc7~jS3fn z_R`N^mKn}U?OJ|Zx7$I~**XaZL~vAmZZ3LHge5RzJ-e{|`qN=E`tz;&O$FA?>$R8{ zk_AE92kU}G9*zo%ETU2tZ1FV2ig``>#%|^t+vXd)+}Gt*Zre!9>PGvvjkXwShJap2 z$4Y8e1Uwwek)pGv#JJlQv@TD`xq2`o=dtsN?RU*5ZfE2?bv|*Wr8NSZXXJEX_|bqt zG6j`G_5wXKDv>Z}o2;-gD`CR=cGLao{f*4Oc}7qx^KV(k&jK_w9eUIl)F%PW(y-o- z;_X1QkY@vHc{U3`BbR|j&6=pHy3`WTs17t8XwCo{WDg$a4}JE@96eYPO@HT0q0ow`9T6mMnF*Q)<-2YHJf5cRWqd zP8Mgy%0G}ECrKc7N24(3{z zAl#zUY<&&Sp?Bu8Vl&NFMlarrXCnR-Z?Zo=vek@><3_6rH^AOj0V(WDbQfoVk=Q_W2 ze(U_!`K|L?=eO6xZ!Ri|UQ06C5OGq;ODz&-pCS1Kv%v8#oV)6D*Xgd)U8lQFcb)ED z58Y{&HYlg071_qbzJzoTFwEbXK$TUgy2ed!6?>?{(gLMZA|wJU1L7W(@_8 zkxdLLm4GjWfFz`P!u7$8Ng$nAJF#|R?Zn!NwG-)))2)YOGc02$(^#E*xZBOz5miTs0ubVvpT)23&aliFLqZpTOLPeN0v6=_0F65qg z0MI>v?g5&xLGpEJcQ#f20ua|Z7Iy{mkT3+=??8qZoz{CB9xY{FGjZ!X+W?rjD(u}sM3*#%f zQv>fC7siY3k-R;RWJ1Ym%E+gCBo$lFYukQ3H!fVyjceC)FL)$NCuW!4(yWQ~XgH3v ziAO@+Bk3N=86F8Z!7@^!O^NE2+UzP;(U?kt&o$l^*cc;5M-QDT#PIq^@yK}e-GbYN!7^G$LI!FbH zy>pqPHPP|;?#|<__ztd1cV)UO(_NYF%5+zzyE5IC>8?y`=0@An*i0s2NXGjFoDf-? z2OOFSN0aWXe{9 ziN&Q*(ngSJ_{ktLuHGE_Uk~TWPoo8>q6Ii7T7Z>k0k%gAun;Y*<9VBtm!k!kMGKSL zncAZndbH3-^I2JGS*j?!v`NVAq*&bG=8j&o&z?)T5>*0IBI z92tGY_YvPm{EHj$f~624C?pfuBv)RL5fK=2P|>zW{C}=Cs_N7q_tGx{IiLb`Oz4=< zG2!K6LdaHH;j<>EDO2!9c%ifcPT)ey3tqrhP?#HKrMtr`vWXqj`(ZnFbnNKZ@shAZ zDWe=pmP!WF%4ii7iJ$~&o^jKhetK7TU9lwlO=7JZ)D%!7rkB5dO^}>ojSNE>DH-!$GUh) z(%j*(!{Zt7=#&ysvDPS}-2cz$oEFlsF;U>V-9O&to6iL$e@ROwi*vLbf#ZV7;u+vT z)4Hhvc_)Fx66ozQZaX;01#pmSwYR}RE`x)bqvZ%37bLAZICOA00~}C@oKZSyBch3b zPy(*?~+4Fo#4Dg+{M! zK% z@9vn;{aoH%yFqe_#XQC01uUX!ccU347_HfILzJtF1?rE-sbqaMv#zCD%{;bnV{Of1 zDuqn?aI9%(#sm1nXapbUzMcn6M&smmF7t!?^-HShaD+J{0v#LLob68BqoGE3kg1lP z-%{h%*~alx8IAu=pKq>C)%Vlu<)@}%&anSQwrB`+OJ~~KnF`A=8bewIBaH`ZY=)dd zNTz_9Zyx3Uy1E#&)|e$Jt8x@Z4_B@`M}=PnDQDfb+X|L7|I+)fh@|3ZMF=)WMk`r4 zj!t+HeNJ($|E=0ydVjMPz$lYONCka7t0-(%7?HWSQ49KBLsLBkQ@w zpDu~^X%y{K%g)D>PaTrK8zh7DF_1SF6l5;}87U_y(ZBSB`Jr3sH=*!$%(G*JTAb_M zG{=0>T<;Rt-cKxVLw{I6e>hnZi<8fCy86c_=N)zQf9vQ^GxVoL^rt!c%S+H-j?iDW z?0lLd+tL3!p})y7l1g3$NWr?{Gzo2!bfh`k>{2^R{6eR^(?O?$P6wS1Ivu<;IsosJ zGfLPPLb6F&tpjCagH+K9v1QZH*~ulBf%{3*D%(h<=ack&l1?hiq|)W^^XWSGSO*<`=(_m`~nE{FHPmpM_54OQ+K(A2sbkb8D#s ziA~W=EuvY)Ye)Gugnxl9pM@Gcfn=>L%4C&s+NL2bPm^?rfz!g`Ly^`gsRnODRG7e^ zQbj=03nNKdqeysVtwUh9ki4<%!2O6a46LI~B%p}SL>La+3QDjv26YlqJ#I?Yk0@b8 zOTuvWfZ$E^N+1gzhYXLDy@$(EjDAFk=1@lYaQbr&K08}L(Q_iHQclqb6D~=aQBR&S zv&jQ{hLjogvQuWd2lm}3G~}r%Gj9W4yk;pAfy*X=&j>CA%*sF%(q`MvQf|*bbl~a0 z(}AZ0&ou7#P^`aLolio-f`}siRUyrH)G5Hb#~Z%VkJL8bT?J zPTH4%*14R80WHstUpoqQ6zV9{QE1x^e4r?@a3*TZ-VX;u#i(s&W5J?=YR;!Gjh-}0 zzSr7(UmER8qn!iJ<$xb?Y1GL8i88wEv^K&!fzo-Mz#AWB3JaO}dot*x&`F__LMMez R3U7=Q{y);)_$i0x0RY_zgI@pu literal 8991 zcmV+)BjDU0iwFP!00000|LuKSZzMOe=DUAIKkvZ;j9>&W!1w^Y0|*e%I4`@XSA*9% zg6)>w7tfse^~)?tRm@CgDyvjdtJSoDmQ-z`)wu7MP{li~B zhw{$VPr#&IW-uPSCqoh~2_FseP?wFX)%@Sz-EY4&D>Bo12#7FynSx?ne#s(*kQKAe zkbM;Ic7K1DZ$G^oO8@%Xmp?uw@lZmk=$EfU4dUT9_q+SoU+%ZBX$OD0^ye?1zxwj! zztgAN!?SSz_Wv$@K7RP#m9opD^Y`z%bYDafUn!t`df&IZGWMU|l>o;tu4m00#C-LW zCM_k$OfrfC4US$E_t=DMe9<_eOf96)O>Jj#}7|nT)|n ziBIX}_0~3dbTVWc302lU#F$7WA%a%gYPSB}AGe>sgxintX5X&MYxMf%`lWsc#zt+A&@?HtcMyF^ECY!yr#jTB%R(dDiQeTzVmJ}saUV$VO z5`YyKLnesjiAi5i>%}(7yjWjFm@gxe^an&TA7ISs={_pcTL2Rt_;lUkDgOBn_RWHD- z;t$UM^OxICMP}ChzfWINqZPQd75Gr6oV7yMt&r_jxR0^CP=5J%`=zwz%Ki2^?eIhS z@!L?Axi3o}v~$p=3Gm^eyrX6VxG(>_{pF9_f2L2re7^a2s9$Bk!8@VqC+XARu*-M5Tpf&y4uQZzPaj1sfVl$F68yvjDP@xBaJnxa3|QE08(ca9=!9(o(H z)m{^8pdd=fU&z~mRuOY@xs20d@T)ZTfQb4Y#mp2UO@)wV1*TO^P6J{e0Fv)ZqPcLm z2FUBK_Y?7?L}kh+EuxJ+XdhiF=!gK2qe-+Oe5o`)Rc+Vox6`Z-NtUQI>1bREB@{2% zS;iYqM90GF^}zHJ9z6ZYoK}lR zu?HxZfY~^O!3HUD2sZ(()a`-Wdbh8i(jX>n1B7gXNgfj!61D_I681Py4CIq+t_GK88m$TlzuObkyT^lLSy7p8uPcR`nym5S1^@C>kn57+=;87h{`A=NQ^*Q z`)s0@Dhm?EDg)Y@Hjlh`GZ}PX?MrMUl=aGD0w;8dL=0z(#*dnLqV%u7UAHoWD=dOJ z21bG)vJ(bHQpQFwae>93!D6q!ADI~=Tn=n)R3u#};Owa2UA6_ULo{;16gHv4soi?3 zGPWLwV3?cWWJ6(+05RqgV;aYpync7{F{Xc&fA0w4oxlD1F@AnNbieL;JkM7`2@1R! zMuugyPyilO_DU(XSjG&Zz3llok6(99zcx(^(xwc}6-OVX$SD)XB!pv#DN0PsLF*I4 zzjSV1Ubj7C@4ZB1Iv~2Z53%sD}?XH?`U9?2zNLAKX^Sy<#-ed>p8h zZ?4`?Ux(Vfs8t4v1&8NNh*~M^}=`PJ#DX@~+VMO!u&W_agpIZxX zU;j})F*`HvGVl)UOk{RZWcF(IKF&mr^YL^gjB&0tPL(i}_!KSRNDJ81!fNx%J6EmF zo3=iy2aYrPr4-Ota~}geYkO6!`ru0Fy({mkspGVte|$!x{a&MC>PeH~dpoLDa3=aY z)N;2T0`0{iIWYvR8XVg+D`>#rBB<8*Zi@#?75>YZv0q!NalN$*HN=1xia=t*-O z>00XBRaCv!Xlo6u*aB9Z)Ya%1&gvA?j)}F7iSs&Ezcx%PnR-_3Uc+*RB610ZP|koG zY4-YjAr~6*-5UqZ%j2g&5RV{;PlTYNNp2y~V*q5vz1Z`_4%JLBYEiDLS%RLGFi!zJ zw0{52Sh~7ds(Ffl%}Bsa!93E$@>WB}lf?0sm=~g_Z=V%=Oc0=vF{9nd8AZ#*s7Ou; zd3gURge*sdESJI}`LwVI&y0&c+^PKGtwUs9Khp@@*NT6@(V4c}jX4WPXDc2p0(e^e z$46#l`r$b6Dr1YQpGv^TER8cL%Aikh(hzNuBr)?a^S`zV`eudVRIrewP)R0lGDj7a zGnQhBNhQkmo}{0PM?b-iub;<|r*eI>I>TU5k#)l!&p19$*3kT|^i?e_MMcQ+sZa-VLBXP4h@zPxy_xttWy zjp;QRlef+q1fz67@2!_YdgSbLh)M~sR*b0{P(3e$%xqyYnlg>au5P7o$x3Au$)#N2 zEye7VR^Uu@nk}=265npM(n*YD9*6X#BRUoXvkKYht^`Z~;PYiZ^i zU|t?RWeF5VOQ2O2?Z%mJ!1HFlyBEK0FP6?>CPqpkD(e*cLI~bDE}zT&VMfbdym4)8 z)q4+XV_PJCd5CEE_##9!U3&UD&J1@EB5+=wdylJbcISkbxa2K*$~<2XD3TEEud-A*vx8 zb;~&5>6tzAjL9+doSE6v;i)k?+D>M# zjyi(bSx3byt{TADLHzZAIL}a+7eSoopgYUDE}v`$aWyYbKLy0~2*eu)E!25-mb=s)Pj_Aw{O)b=X+W9ljMIn5^mzqL&{q-66 z3?RXsLS8wAG&o?9LYk02eSKxy&6Gl>8OCLc~BE z&N6YbiDCjC)@~9gpIvY%PV;>VqkK-E{&F>=)Vo+8F{oRa8^WVUI2? zE9r-#G<^W9n$q<8>jRq2C{1@td*zfiORR&%%sMc03Tm7*u$|JTM-SNHoPj6oAr+%N zq}5j&DXluWpi^3>v;(D?D3VWFS_p`!3#$oBUS-V%Q)Mjy?5coktGVvETGuouy-SI$!?ie5s5|sDhS6 z;3FERK#S;&FO21tneC-~gfCB-G^x&6x*vday6be;>8{gVr@Kyf&qH^~pkWt8;W)u2 zrXj^EMH8%s;cVmC4#!jJZqea7xpi{uQ@uv$5d z_3hpSvVtjn<5`6%edAfjl-3B@*a#BTpe7xN3HdXa- z75nru)z+=|t2giNj(6_f7rAot?y=gr!r%0@=1Lx&;dtT8ULMQ68=l;F@x9Iw39|v` zit=@`Xe=uqtdHd%7niOvUoKIIL`-0fEtr;tz$~r66i8+v!7c1`e5^y)TdR*AOmdvO zDnF7IUV<^+D9K4C)EiHqegS1(U%u~bN}%suGFDn=RT3^EhomgA6~eyh3(22bwq!-r zBDf$$vTS{D#bdNhAvr=8w2Y%K4}vGp#{J;Bg+P#u&)yU#$wWG2&!*6$&DMGhC)_r^ zi61vN3|&shl%(`3Bof+463&(%&UsGZV05>?rv1(0qmcBV%=)JD>JFK^hwg5eEHP2N z$(vfQ9^=!=^^&{EO=yEum9-^FfY$xWw`5>iyrRg_ps| z=7#JCF85#KyeUv$%2pm|HKu%gXw8Sg$!|Xm;ilMo|E#_fgak(^-3>G*ZJTV-Z?=sl zZMy@Y^2^8DFNg8t5JKK#lC4%K4rX946K>7V!9H4=xJp?*Uu&Z1ZiaO#*mhQ1wwLCdFx#)p@Y%wgO^YC8(!=Co!`(=2yaTjf~;~X#Qn9| zw#4#+k_kHHGFCxmUS-1p&&;7pJ4aAk0jO=_r)@#|p}#+uC}sfp1A3~$T{BUs%fx9v zuoV=vlPXDOr$tsJBo}C* z3rLo-l8};jTBf8mlpt2a%0k!M8n14YmnO%t_&{(V_ZI<*N01+>Nhbub!El zntNPS5&J`N>%sPMVh4{FcUVds7JtNa>99(J1NS-IEy?ce=rQqORB4rfIy^fmQhYeV z%4C_ep?^K;_hIqU{bS!2vv}fPRYtv9IdQMyxWD%^P3r2Y-Bc*1*@5Gz{rB70m@QNv z+}BU(_o7Jk{@7l%aEqV{<^XQTri8V`w9uFUVHa=yYBYvQW6C$BG4#Infp%l)DUJDC zRej6M>JL{6+=&9k4ybsP;+z$-3Mmm87Lv-a6>T!@QR|C0(+P4RL}hX=W4(wuWK}35 z>f}M7kfUavDE;ei*DVExGpY!v0%fN$O36`ZQsktM?Te(J!(y+$ADN}-Vc`*qjjS$YJGnXNG@0|ep8fjMtWz@-n)8G+W8!x&kzD84Y$}`%`LZSDvfDBtF ztV9ygJ4Y+y_}4wustW%OhFaZQz7uZ&SvWUSMjg0BRZ0b`9l2D3E3a@Ry?bHu;uYGq z9NYH9d)IASPHkIu+x}i`yO_3!7*zJo4tEmfpuDkIm?4zGgBq>P-rU@@jT@%>a(KwO zIT}da%HxK{)tv;h#Q#xkduu&R9{w-$SX;B0(O!p8 z$*QU;j75n1J=q9H^qg2rscUMRSlK3?ZkwetTr|#7$adqz1>?juJKRVTWvEs|wEdVc27__HMVwu+?`8Y3=7v+3!)mH*Xl6l_j@q z3p}!gjeCl@s(C1)X`q9GxSFrVwf!^pdR|`hxwdKXqP4G;wb1n=92}mkS6L_JAD&j@ z;zoJ7ysQ8<1!k;61*|qNsY*s_S?20${P$?zPJIDQ-Sk#z^@nRD-MZsft;zjiuhfe3 z)LJ@guas?cliNoutQ~}5AI`y8X{$M}t@UgBM3LQ+krkWJQ^c&oThwi1Sd&h9X*qg9 zvz;K!0zs@gUfYSyGC$Z^6KlXYBIbl2Y>OW%d~MQ$9XpIzY?Tz7#Uw>rOmfA9_i=es zQnGa`fCZ(@Q^UQvOleQ`n-hcdRyj_tZ}=naY5F&Vv_BUMONp?>?Di= zzKaIKe_p7Tt)X$L<|482sGLfM({3E=D&Ksl{w%?9Dq5`?yP$vCu76t4Kb@|Bs`W2l zME_5!WxM|6h4e2M^e-3nFDw1SR64s+DAJfBS!?295B8S0;??fKK0fjIu?{NPoYA2o zj>FMl2_10qAW_Pc7Z%~(woG(n=Om?Mt;HebkG=PpZE&bX3FMn|p~YhLlELcQUaz0W zV5b6nv&wOhTm+p^V=+?=ARLLyOO*R^e zpNZme!7TXJv$0sEX6$Odn3^T1U?@Zf!k|%72osCWEgLAf3YSvz){v+mb64)=lq<79 zViw7hR=KdGbT%5N1W6K7Z&)kj-S!EBh53QC>4A1EUL7dZE#jgU5opM*fDlzyntd>e zi_?3dI3meKci$E<73oihc#V^ny1q`(m(R}Hq=dy_2}CRrlqlg-PTEK#m3-zPs%!M( z8l^I9i;CPweG$(cZDGn_`JDGDFUmn-Hq~de1SGjE?Evp;t+csL0 z*`ia0?+i#6wQ($%OOWh_bIj5z^Ib9_=lao%oJ;2u+i#jr+|I~(?tJ1(OKSu+&&cV( z@S_1kB9*{W2w4#r^bFEQLrEl5QarZZbboq(BlB;b5!A~3TbA*Q0F9iwo@_YvNkFsY z)_X7B4m1mSHn5gwvj8--3^Y7zB3E_s63}o5nhrE)08L}Yrf8j=}eH*1t(W)mq%<5EsqDjt?q+NapBwEKEgTgS_emmM!VUcMc?^cIHX zZjTCv|LqVv#_YX`Lc8b|E;^f`-$>RSD?3(ptn66%*053lN+mVupaOcZK4%quv{phS zWm0wHQqzT2jsF7YQyiz3CQFFp^C@t_!xtQ?I(n-*pF)lttqC+!SDT+tL5+jC7A6R{ zsK3+B3(?N>fC{M3Upwc33RpRy0=8#B!a@q<`pGbD+F3rJ0%iwPKy^R`EFDk*mpP!K z)6S1ZI|UOwT0;g@1aAlfgD$M200juvkJ8TUxT49=X2Z)%^}$c8Apd^E5nFKZk>}bj zsje1@@3j-Fo?~cDtd%dx$DwqPx$eaJ28q>7sm3%&>?C4cqOm<|Z70@+Tu)d@_FVE} zyL|GKn4SDopE7kUd2;eo>x86EtesdNKcE5=BsW}=0@iw=Rg%M4E~nsG_=;FNzjc1= z{MPxc^IPY)?}y)FusJG7!Y1Ri$x(*vAZs0g%Q$jAUwJ>AyY6(?>8{gVr@Kyfo$kIL zx^qGp&jt)SqbMpQkrZg<9Y72r&gpJ4tJ!(4^Iqq@&U>BrI`4f)ya!2XmoTxE;4~$t zg2G{u&`KRC&3W%~>w_DUKsvE@V(rA*iM11JC)V$XSPOXjkd0O;I0{0r(9U{Mh&81$ zprmGQ{3DmMEip*X(diuAIkp^N~M*#Yq2tbb_fHgLHKO(bj5y0wmZS2tBZv=I}{G}nMW+{7|suf zKc=(8Gjm$3BZb3-@oHH|-$z8UM9ZrYi5*2G3wXHS5LZVetD}^sj%L2sh@?5%sxFML z% zO#`>zrhyB$Y2fL%Y2fm08aTU61FKWJaOpM;?6+z3XyvRd22rp=nk-WZQB>hOk&uH0 z6SLGHx6GeBHZgGVWl1oPj^ul|)5Dz}?(}e{hdVvo>ETWfcMg*?A%>XHV1^V)*{FpR z%tk4bl!b79xO2G`-ywAAp-c~DdMMLFnI6jYP^O16J(Ow9+!#SRB%!l_7!_EIKB7`7 za3J+YzIa9P1q&J3SrrTl zLZM}l4y3{)$dj;X_2$t3dOS~lI$D5gv;gOf7GPzx0NY0kurOL!$MZHPFOL>rHd>h6 z&eZm1=%a=1&F6Tt3eIPzJeH1ot77ILl?}|s=TN%w?vLBgUuIk7hQPTpK=;R|bQjoR zIC@6+`0nxD<6oV}YfwTcX{0oqZP1z6`KUA4Y)r(q$N%SQqpD8*`5^rwkOL|}$Apdv z9TQ$JCODNtlm?Ow85Cwq-a2M-WSsW|3sJyUP?#HKrMtr`)WnYI{jeQ7I(BsIctzOZ z11HD=Fq1+qu>~iWz-TX>2NHZC>^Nwr2^}3II!JVoc)cJIL?W`N6|0c6@Fm`G+8fKv z(Zp<=x-CWhgCrjEc-^jkdFM7MA)q9XWV{78{3aX?}jjI)6uCXz-b7wG^TDgFB8zthJ>0MWbg zJ~^rro|p5dtHV!s=9r8!EgQt7aHu_SRoZP26yti^a8&ArX}$HeN2e#H7I$7sO4Se1 z-7%s2rJ}obgJ_DydWyvhSR||6jb@Z!v}Vf%o!2r*wE%|cj6um9^FC4Ejz!X z#_O|<=wDrA`K9moU#rvM<%3T z*pba5X%0@xb5XxrV7I_+76_hlwlOD(l7iI8k=#nC>_NBit4iA5NCU;^Z?;SO4_Mc}E@n-#Yrs8T!jb^p|t=r>CGljnJQ3c0SFK z?dboF&_C%!A!P?yW@nR;*?W&!TgyRN3hgZMCkEx64murlI_PxJ>EN}|flX4SP(Vv5 zwg@t_O$lPiS!gY(y|eH_$t6z%_mieowvkHDC+Yblom7@drRS4$QrWZ+8gm9Bshvrr zC`ln`$UlfoCV?<@!t*|FF{NJ*IL2MAZ3PM zcgjqUz`pr}2A!HR^G4uB$fTSW#3A2Xy<@) zIp9ZJ8Wrqg4lW7s(MKzTCMTmUgJcVk1ubOe@5!K(LMMez3Y`=>DZDXK`2R=kmy(C( F0RUxqed+)J diff --git a/examples/hackers-delight/why3session.xml b/examples/hackers-delight/why3session.xml index 4e08b2a18..9590089e1 100644 --- a/examples/hackers-delight/why3session.xml +++ b/examples/hackers-delight/why3session.xml @@ -10,14 +10,14 @@ - + - + @@ -30,14 +30,14 @@ - + - + - + @@ -69,7 +69,7 @@ - + @@ -83,7 +83,7 @@ - + @@ -93,8 +93,8 @@ - - + + @@ -107,14 +107,14 @@ - + - + diff --git a/examples/hackers-delight/why3shapes.gz b/examples/hackers-delight/why3shapes.gz index 427ca350c5ead4e165bfe9a0f1ae2e03b232e7dd..d72288e9a505e1b3eb27c71aab8f457a257b3898 100644 GIT binary patch literal 2847 zcmV+)3*hu0iwFP!00000|Ls~?ZzDGne)q5Ndk}zCyn#&+V*@P=3?>h|=vRYBaYleg z%E$*zC>GCuV6(N(8=-()Oa}60^Y_cLKU}s3xVihd zEywNLDon4t{;t7B4P(jU?m6&%`88{nlb|u9!-i$1QJa45-%j7(Gcg>- zvcX}(4@pe#zZ)+S^mFDSkKFAFcgx(__`!pgj5LWhN{d2~$B4x#O_)&j#&2Eu&tECs zT-`s6=0EOl?zimr9xbgEdS(l-4pLxe=i|rvy=g>?+N(2Ln^ED4X&7&>OxC?#{1k?< zgkhPj%i!EK-}lQ~qT9*hHLR}jn#t1ZXBsz*ZR4&7|G0?^)uWBuyj#Y!Z$Pxx8NCI} zYV+=S%K|ij4ajzRJKD@*@+Blx1G?d)(UPbm_R#esE{B)89Bc!w0pC%rqfG-RSKi+; zp+>x$XOC~im}rp05nG1ss0UiV&-G#Nyl6Oqd0^4I;{G3|GG zd))4K-zr#_j9RH0*~@gj5GtiCtk+fu6^t-0YC&j%wgAOuG?!n(VasGLIny6FXVbbF zuiq~y6IdxIQ*a5qD1w#dl$%(8fk~6S40m^Qn5o(UU#>@_T#d-y%#TK-dNLyM&qU;m z*J?z{A!>hWRHMg;)aMbY*CNtz3Y`a}eOWxZF_`P%&j;f&o?jyvS3pO;ZOx~UQz<#RUs6a$bo*{s&=)dJ4f1EOZWfL(mjh! zWhv^EA?p-~I}nWuv(Mx$I)iR=_OD9whI&s<+*XLV31nov*xH@UJ_kr|cslig&-79VAcXKeAD zEizk8S(Z>-<|aem6WKWqnmPDU^HyPMwa!(r-o{kdotZi~a#uUvio3T<>@5Al(`1>`3xFhxB4};{Z z=w95c5wS6L(CV7@ge>nL9CVo80Ts7dcu15yHZtw-(M>$M> z5dzRP=o|S044@q*pJ~C76~Sn(P*ceegejD4q`FPV63Lillk-QJ+l3PN(sW~Dv$#a_5e+im#5WnR8&hukF8 zGL_rkTW)`cru8=59pmCx$32xE;$$^UcE+>@0k6iIE9HV`S=$%`Z%fn}xN z68ijpB2*);rdROG>>l4dc6kPJwbNk>G$D!ve5qK z*j+CV$LbMPwamX3##ADnCT^{8< ze=W$$5q_0G@J{B z2`M_Qxg`ddH6g2mYec)g^F)4)s7p~pEM8c{-96(j8!lvp!Vs{q@C%|R43`_;mbuTY zuUidd`@5TqY;-BoN01@P;+2dns1{rj1KUO01zDyuC0i5T3Rx?RVe^?-NZL|DEC?!^ zru!eNX|D+tTL=Ish%lGao_x{1j;lg}Nv ztFOu#r3sLCJC#xq#W5{L9u=>hNFkmp*ZJ*4uBG4%iojS$n|XJXpnc{v5>-`A6(wgf zj8ulK%diX_KOyj!jrwW)R0=B8v}J{o#yOW$^t{XvN2PNrg^6V+ zPM+HXPWJFoaGKzpP<*yNDHoF9Jv*>nQO8M+n0R@W5*CeC0sC9?&d*_1*zuVa6yEdp zG>1)(;}iB~38DiJ7-g8E2{z>D4gcfH-gD5&0t}ydN@!P&^314KVp{l;J&PAmGonqv zs3mVR9CX$zv+(+$Z2g9*??l1qBs)vXXp=*T#U|heV9dI3*O(-S%&JBlQI{|8Guz1F=XN`gV=6dY3eAA z9@Z}H^U%{kl=X$&98D2Qb1vd+&NWF=z~-?iy9#wQ&ZqEj%4Vey0JjIcw=)PJ*E9UY zH3D` ztzGlg_^VTwbY+K(;i?KSEL;>eItYy=cqIa(&7<@Du^xO$nYg4|%5Xd525bBe422`z z+)^2`I58S6a$gacL9q&rv0jK!NRupQ8~a4pDWBU%_#Cz$K8}ov&RIACHpX1E;wqjB z@~Hk0!8jT)P{TwG@p3i2J%o|Eng&Vz^`tF^8`<6OH^I}xt0^$+S@pXOv^L}^y~e003e4l}Z2r literal 2850 zcmV+-3*Gb|iwFP!00000|Ls~?ZzIPMe&?^yyJ4WK`UbLwg%}J3EY=SR=2hsUdY6Ef z^itGX_ODO%4Cf+;lI#_NIMItZM|YiHU9C|WLea(vqbLPXE|35rJQ`onCcFxpZP`3t zy$fmguswv|X}@d#tV%-bgDu{w1PN7fi71v7Eo33ljXSpwpLd0Z+wS+rMl=w%hfgiF z2G&U=iAk)K$-)H*+F zwF>-e|3KGI(K*ui^5F>r>s1tjSaWSWfw4gz|ZBM*>m%vO?tLTU!OS%8Z$a<*k&5F?$`e9`1?H*!{J&s zI4pRV#Ps?5@g_mPW-ju`-7avq%zeGmNCc_`M2sqyVkuJeCWsuhDy8(sZ(aG%Unt#P zKRk}+KkRNFHthBuEv*%LW@lg>q`=P3hfno)-G~;o*C)0%qrw%_Fg{*btb4uqEezKZ zhHbWPgHzXh-*0b;ZYGNDnxHX5-uY7tikEviW4Gb?VLqxufB%;hRIxIN_)=Pv~0$k z4`-C4m&v17b8+V8Ikx$B67xS zF(Tyhd5otJu&I8iEEFRq$%=O}r2jh7>zeX@Fgm@Q>&w~e}c3B2( zCD{}T3a@kWMlwc`oLT_Sn-5;u2gMp;jMk+D!c;Sr^4fsWnJgtk7k%(5!FAqXygBxj z94ln-DW`~83nQaY(K+JE1YC(Y=-kE3{K8~=>bf^P{Fmc_kPE-^fh13uJQT*P4b?nb zY>ohbu2P>4HE-bgp9D`tNcaCS(mjh! z<21L7q;+)2lLvtm23WqFLev<`)dktUZOB@$e2h?>52y=JDLE;vFehOX3gM&ck2^kv z&!0EjkGJ=~P&yOk`0}Uj>}@K~C|5;V-jq_Kq0wJ1$vF=nhGBaoRtXXTe;GpH!0>TfE2?PuSuq zTV%G%3C=cBnhY^x2m-xuB`K5nQB2QG*Z(XZg=3YOM;}*aHa8@U@LUMAy8Y8QLFUu6Wh?6o>^+K>Q#Q7=fZoe7yIU2n@Y;SwF4~MDW_2;5pxSbug{>j}pPi|KW+ouPx>ikeu zedD1j&%LAyk69ww5DAsfDV0LO7#_G1N$Bl&sE0Bi@91VrUmn8U=J4AMgSaF0!@EK9 zMRcD%tP!@ba*+RrxqY4p3`YAD(3b*3b_>VAc!FftFg;Jx_N`S%6pjt!v$5QkIxbz$ zbLcB1FCHYvSx+&s{IhILSJ+;_Ru79$GRd<{`oqZ=F!AF_=Ar?gbv-ipb%QVPKFVS7 zix7aWLEp$1U;yo~_(Th?51bPns(OlK$wU*0n^fQym1`6@hi6018|vRs|CdL-DLRLv5iVo2^Eo4L>EI!Af*$ek+vk70h&CA#AB@YR; zP37_Tj>q3&XuS*fhqyW1EPM!Ye0BU5LS?UH5*f2E5rmMMN+w;003nlss}lm}oqkK` z%ZG_jjkuoP!OydoFncNLnIl<25h?OGF1XLlI%}ShEk<-EO++aB-RFPo!*85n>JN(` z#&eVI*|4U*T(8h+a*?SxQ>?dzCqofIMyE(e36rlkW-1;=~D?#{D1nP&8YkdN=T~cF>}+TNgC%pE9eDjTX@PW z@=VeBw>dMUoGzU>3}#B+Z+<6Uz)s|m$E7HIEW(E*r2``+3Wbz;vJDrw54v3BJ^w7o zYv6#h-gs|KfhbLJ*@JPG;X`I}M8rY2-5u&r*ydL5HVlu?nd(_CROrkIi` zS#eNVMqUDCg%(RhySej7eu-#EnTJB-sHEZ|1Zza}^~4@L7B&5b>qzv7;d0Amndi*< zxz#|ne_A^P&R9BlLs=`9IRp_%qyWOI#FjWC%XFq>YrGI&hVCQwlcid8H{Ha>Yy zopTvRDnr&?uQ+c9vQ9Y+m^_=63zU_TBQvQ~qksWd$R;_1dp=0SW#ppX|#ykq6BTd#AGmtc}i$^jq=Q>wn2VH$wQuAo7NphWK#+p@0 z2sTyV1fXNm(sCLUL2;%Ai&o79Tp&8=-ev-oESE}zBG{3@wZ+S5IMZYSkjR{yZfdhh z2oIO6w@%r~2$>DX*#)K7%DPYpO%z;2xkJ38lMK}>r?t_}3&XkGaWSfAe~dG%r>25K zNez3??eo~vKz2UWzQh5j$TMCJDiFh8M$5TUcOB|zoX_F$Xjx_q7&s4dxYo}+lCQBI zx%zX{6yq6lZkoEC$#5?jz=KTEvKuISZMiKkA)=2ssyzCm{?=+wQK9WsWyD!{Putg#_Zjoff^55w(aa>8gE0uK~C6mrT3e=ft_j2kTR-!l{r zbbCi-$l_eXGlQF~HQX$gkU8}l5Zpfm<1*Syx=#7rUEs6deEc*p%9gxH^<#9d7(iU0 z1$&-*HTGChQVtlXVWNh3xt=~A!bn|DgQWiVq-};9**))z;PK`46qt2!1?Jh}23MA{)~GK404`N? ACjbBd diff --git a/examples/queens_bv/why3session.xml b/examples/queens_bv/why3session.xml index f9ab1d7ee..b0538ea97 100644 --- a/examples/queens_bv/why3session.xml +++ b/examples/queens_bv/why3session.xml @@ -20,7 +20,7 @@ - + @@ -31,7 +31,7 @@ - + @@ -127,7 +127,7 @@ - + @@ -2192,7 +2192,7 @@ - + @@ -2208,7 +2208,7 @@ - + @@ -2334,7 +2334,7 @@ - + diff --git a/examples/queens_bv/why3shapes.gz b/examples/queens_bv/why3shapes.gz index 60a5277484e794e1d9a87eef34ea483df8aea5e2..85751ab158e7e3a8ed6b0af2cdca2da22be587e6 100644 GIT binary patch literal 16139 zcmZv@1y~$Q*EJdf!GinXNpN@95ZqyK3o^L76Fhiu3-0dj4uiV|9bAIzAeVFA_y4~8 z-2cw*r)uq0t9JKv_jK>->LH6jeE09?^)zEOdWR>j@NA#pz+40s>Ha!uc-Cu(^Vr}fP;Qzpw&h?59>?x1HMEhG{IFu5t`nwxg{u*I#=#V`?A zkXV3VL-cQR&~47A>diMey12-Mg}LqgUantG?Xt2qy1W9YFP4JPgLQQ^VY=aL7?r%MVZKkt;4hZ>K&2jR3=B(ja6FRxID zonZ^%w72I=*6tZuhdUPf>-%+?4H>pt{2Xe^^!rfcjwTF3QTL93meXV5%$+}`0yk6J ziZw-renM0RUc^<{acAg@JOc6C?+tzY&(F`9!8#<&lU6MG<(%@6U<;%DdK+)c(iZ)# zq4QDbM&D#s=EgI0_59(vtwzg|iEL>9=I{Rbt&=y^gA2#0-^-u&2y~PCp|-m$NU(~7 zUVSH%C&3w=;IX2U-S>FizMGH9MFp8GXCK^E#H}pX(mb1=w5y;>_+1Of2FFXGy>SQ5 zWX0HD#SR$KqH(m=T;QSbl|D<(Yo)Ldv$l@A7sxroFY>IYpD$N+nj;U7HwhIMy&uP+wO;GKo=_*K7qRXc^zGRC++P04?n;qcUe4PX z@ryb(fTZ$2JZ*G^a8I83+6f5_vHPuY&tlRP$bU)rsX(TbwlF$)^WO8IgU!rt@4~7X zkjG)flASIRCCaQz9r*F9zp@_3(530jAQ`va>3ni9L4N6`7PjL#n0vQv{70m zPkh8EcIShgC%X*vq;P20R%V1=FauRf8^6>?&G6keTjq9JO7op4Ew3Xr>H2Ia_88vp zXIppb$~{AjC;%8!E;&6s=kjJ>>BXn?tyZP7m!JK-U+!M-pGKjIS$?)z!mm#ckh)ht zr$8q;A~Gew#tzQLOw}&FteG7r*Rury;TGgfc}Aj!Q${GQ^R^HB8@|WGoq+&YG(p{u zHL{kqcj%J?iPbdT$}!nR(fzD&xa?d!?)Y=6`MRvxiw^+ithY-zENh0npNlyQukX^6 zg}2&c96#|P$S;fO8tJ9;`Vu0Hb>ng9SVxLmcwk=l*PLCm{*z?@_XAkNxVZXW)?qPjf%BSMUTVFbD5?R){xI|z-rRkmVeTowD?v8o- z(RGAyk`O*QyPC2v#4|tiqw*0AwC}PS+G+49<(gNpl8jrp)o(rTxE%d!I+`4__fM=e zpmR^g>EpUog5k%IVz`j=K4>5*Dd4oH(PnI?;${$uLzM4lQgL1_UfHk~KHv%QwOf)V zTM||eV~GaKX5)57s-(j*)D2g(^Wo;XX!7N`?Jw`>JM<;l-JDvf$5w=ZvuP{CpwEtc zR6jbxM1dA(HCFB9K9r6&?$8(Ep~jHtF5MdZ@%=mDS1#Qw&7KjrGhs#NW{+1UZ^HFK zJPnFP4UVa;jrEXV@Mn~-dT2OZcM6*R6|SGI=kgA8j*Rp17iFKGez*TpS9En}Z}-lI z_?;IWieJU!jI4s76d*^f%Mr?|1X|zorlFH>Dkx@Y8xFD;zc>@J05fNJp-HTGUFsaj z=)!siCPVyM(J#j_i~g@WnZwL~>}q~)bzkC5jZ28>Q`sS$db9dHkG@7d<08C>tq0B| z>LGqU6#KE`y6pyo?Ha8(W6BMea$_WbZK8+$I@XH$&B1l$VEAHbCjP<;G+OVxYcD%; zkLb87UbO3kKslWLgRS$Xl{HOH#=0w^IDAExgu&C8uiBF)F1`>;h_X;{?-5%6<4T9vjX zXx1^P{svYvK;OlqjZr(|(i}5k`Tw!64Lxoyd3qVTHxoA!nfXx)T%}>P__ahUcGvZ+ zJBK@frapkJ{)?luX)uhiWB#N{jjNr@kAfP3HKr<0Hq6tcMRYh6cr8Xp>l04RERZ4d z41H?$lk(B>zMK&=ge#23@nMS~UTo|UZD@y6SBO<7(Nf6rE=xj9|c2xE2ODz@6L7ml0RSU%*7=SG2+ zecv= z30S>7P0F@d1t+_x6ce>iup%Rk=h{LVYO2TPFRi(dSo=Oo6*}FYo3E%)Sl3(I(?w-g z+Ri@9kwL3n@9W;Y+d5w`{2se2o4zF@vpYT7w5-;u;8Gh~vB(P1K+!CG;Tv`3&Dm)7 z=4;#K~dCizqaf8Fd;?)lU%~gix{3<#wE2?zP zX;bl)<4srV1)%kU9G8_*E=1wRbFGHx*(9#m^?KzY_#nc zUySoQ))!u*dKd?oj58~6EzhQ9W8}|&cN3EgrHw9cZQ{ukC=&1?#e(nz%^+B)pcKaM z*A|}wnbN~;(nh%C z7|W1FmALcYep4+ouT(J(WK@cyVf_uGR`N`Ral>lF1?j{E@nTu|Mcogk z@$A63kKB~_XxnzASi-h4+@0k2hf880p@peqtNGoT6QOl}MoF3vSkd9dCkJV2eBLq~ zsbx~6p$)$mO4<*Dfc?U8>_@d0g4`9ESn_}Av_e%~)-YG=6q#a4DicVU01p@G!3z$1 zxh{Xi<8?!=xs>n$i4?ywE)Z*d@{pidF(XZ}t%S~3y--FtH zbq2i%*XKeT9V$3YlmacKKdikECSNJ!URcU^X5=p0VjPL*_jHQuEFxg+E##uKN_Ow~ z`mjSS{e_@{{|fSlbda%#IlUNvj>-$ zgS;4)8qatmAL&q0ClB$mYkh|%@NP-JZGrb_Ice$5CYG^ortRTA%yZksbe@VBuBNLa zZXiv!aNBKky}HnT4S)5_938f#n=be~Em#ZlkNpK?-@tXEN-fY$!=w}*ngnKiHp^Zd zkA}${J6b|qelxcyr8o>3dKd}%D!B~;8y##Vu1)Q=<5En8xq-x~;M1r#vsqkMLO5x`EGDHYG^9F&1pgh<`28WmxWtkWxj6jX2?o?{*U? zF2hzMd`GW_z>sGji+V8f?MEWBB9B($FX%{8ZwlWBlx4+l}MN zdxPR?z-y4sm1&bu>vk94WKk6$0I6zx!t-caVSFNkEJ` z@%|V!Eq{Vg+Zmk}{u#u@{$_Q0?12j+W(7{`@zWPw8J5J2Kh$Xto)^G>h*Ae3zvD%C z5rV2p|1R;*2)=i3KXE>>`Gz;i3V7I2>vDIA5P^S;TM+uz?6OosTin!qEYcJ&=G z_!~-$yQIDQo$4PjfP#}sB9mFKX^JSqCH77|6$zN~VQ1`pbjpA~o51xhg5!m6C$Xa` z%*VPPky;`n4Bt)hezATm-qBP7;r(L&D3$twLLX1Y6o&oZ_JR0rs=6NssPRt-Zyasi zk2tOFeumBHvG??7gwzO8ymj5-frBHW#uE(HY(NLXQpCke<|@pFL_L;}a@S%Jk0Vd| z64-os1O0JSvV8`u8AFB}%i8VQ+@+fXF+v-9>ZTYCXJ@Bu`xZ!`3FVKT)ZJ+GZS zp4s-R{zj9b8h>23N}TT6cAq8vT$z-9{6WWQA!3N39Q>m3Oj#!aBc1(&QmMNMm!=wv zh6NqR9fzj$@5RNDR1B=RcvWxx->=uxZYVhE>z?P6W*wY=wk!7Gt+$$IMYeAB?i(!9 zKZJ)<`$vJ4uQ!EfDPad0NgRctzaCC{dlVybvzv{xm)s7uvWso>*pN{B1(bjxbP8g) z7Ict<6+Dz?^=!o6ySdasw+fAltHJu`baR?3nfO!}5*TqbLShacbNi{y?2EMzQSb#w zOXk^ABS|ZrYE&Y|ZH-o*O4TbFdsV?*I-JVH2IZeF7W-tF9Ch2+^rS5!(H9eSXK;}v zqn#TruBI4PX2kwtDyY^kerU~eQ{{%|>+W?Zl9ibOJIwM;MMc|@98|tkV;wMcEg?JO z7o~n^Z6FiGJeYeBDMEXnv4Z40;wbx;DEpN#OdV289a2sm+R;y?%4Co7Qm5pJXx!Aq zXxMoZAJAPBQ9Y87JU_oD3Gan6OPUZKSUP+U=c1Vr(J&Kk5DERo9VMMDt5NZdA$_pL zLJC$-ki{CFkMr^FVTh9YTcTv>XOZbpN{&DDQ)(Qr3d{sb`~H=2;hPEJ*(0!epyF)~ z;IzVQ3dl@)SYPL780K{@_2Sn>?XU{#NZBTuG7yqelj9TQe&`|wLN+8E?YE)y#Ll*q zt&2cHgI;0TmYrr8XgwqKsW|W+A%+-_m%&kUr+U~hwr~3m8?S(EPDjM1+6I=lM2uPq z{y^S->LAF^Gnq<<@=`^L8#Q5Z)WWyGXtdL=0|YQ_?+WqCyIP5Co4ELiV?YB0AU{w#2^t8~skuS6xnV=S z*(K3F9bdtpAF&DH!%FDZZMG#eddro6Z)^521)-_Gy#pAK+5`HO@rehERA(jj_w63c+_y7{9P8R?US0dD7QY9g|DZD)U#QP4H*QuN8;n zQ_$Ikn5e^*BWhw+fBr7s9sUEiXR!itxLzXHnINI26m}zhYmFlXZ|W`~$x3ZcM-<>$ z6*}`v`27wgv0a(}mf8;U$lm(9hrRV`YZRt&7pF6VfjXoRwfhWP2m^h(R}nkkU7lG2 z!{Nxc#+EylmTPB*VC(dA9nK`cm;FBp%YWx_Y(slZi1*09+L~KmDW_#SaefdZkOi6&{LvnGFxdh{!q4Dbwvyg@@kWYSK8Lx7qp|>b53uTNFKMISBgQpXxD4;|I zCUHywXGGi>EV9E*^J$^^?fL$6l&BnUvGiv|5_4o`l?qDoVU%1C%ANEUM;97OHT*fu z0l%FH!6eDAnh$jb@9ZO(`Eo_LD^tI5I$Glwph`w8>t1_`;y6arROBXB49?NW#Rg-Sw>`Kz2hd3~{$IT54ri^!(fhUYwgNvw&Nu_1cb zkuk|2U!)7cG0TEsd7oxz4H|z*U&46v#=+bMmL=u{N2mS&O^oAltDdETk!~+TCK)= zVi!Zt_cW9mo`v8*SoSX0h_C07JA9gA-gCk(IqA5Qw!&~4$a*@6di<|khZgA{*Bz6qEB8x$GAHfSdcP!$KLzWg|l0-VvW8iU#up?`}b<(U*u9s5ne z&E@DZaaVMT@`aIQEVZSPS2D5ECpaaOzJ@C6S-PH}Vr}i&a2i z)g-W{0$6ih8E`hL$HVN#4$=jbS`wDZ=p{HzDd_C;OOC(u&#_q<^lu3ID!mc1sz1QI zEvA^JoUs_mr^`n{CbyznuTXo6lipjwvYSrA#r4al zo-DinBKV+!o7J`F5|P3H6v$XiFA0|%Q}h1nken$o2K4rk4$=X74=^Z?r(NUW`c?lu zEd#cXw=HxA&c>5$q^&DU;Ccz;R+)UVN&fPy z^geAkBi|XPHY{8NS2)i^et>=~U4Ok5QY?ZWtj#6wG+R=&rqq#6rysNJ^5QV!k}y$V zm$O~eQkVC)BRRYZQI``*7vzX*pj>UKQVrgt>tqAYa{v?58(CG!ao^SFoQiKC1P{7K zv4`YlYrHooecP;&l-(ILs)c~@gve!8HiWaMaR6lHY<@ zQ?7OEpnd;hkJ*`cVtn5|EEHGJyRC2H!Otad>&DUt||bhBM?Ljt=@NW zO!7(j4Al%Th|lEmxK$2rYce5&V%&zDK+FNvizZ~s1uFWNP4i_y25$AaGx_t79h>E$ z3%F&ibKk7xA)(zrlR{`zJDp5Wp5hF2@>RWjm-(j3@K8_@ZzvK~zELJ3|3L1Y(M8!ERs-!puQz2!fCKv*7v z`71afbPG5qsf%$oM~U<1&8<7h`#e!a`vY7XLzi1=O7?L4v7x=QTbY*`+-mLV>x0SZ zp5_Cbe^kHCVa|m<8tYxsFglLtn~?qO%UwK6@Hq(Yo{#@I#WpJBEZ%b@-D5dii>?PK z^&~7MEW*vJU!3CJ0nQ?eX@8JjI27?W!5G|K9vb+aL_T&1UqtlV*1ompaL`*@ftzP- z(>ZV!^&jBA=bR_U9duKO&V+W8Vws};5mBZ-<2_K+?P&aLd}x1fZJ%53ob2s+qf>jj z9fv8_sJxki)dNo~WhLJDq#1Uef1-urHnl#KaF1rO`4cnWFlVQTetlQYFr$aEi&%`u z35ne*voC)?H0HXbQt9IY26tMqs39)86*#7|-?HTTrfPb1Cu@Q$)a`N$UyS=!$ zKkpHUCesgNqp_{bn+O~6Kia4Qp~-!5gk8a=9dYP@P}OJzxZk8rLy-yKsiU7i#PD7D z5v1>&0T$gj1V-mw8*?+S7`)p~^qBU29;@((r7LtS2KrRKm0%#6S{68`vB>eHkRg$w zKuYe?+L(QrS2$6OL~d7!UzHbF>Y(vfawUpUs`AdUC5rjzytyE{P;lAx+%zyc@bMnf zUi_7G?i=ZxV3DIWH8ov2xF+j&H{;029}%HMu_9I8`lU(DN_jI?-lJXlbPvo(>A^Uy zgbEW6$*}$Fp#5u-B1d8qmgO5YobpVZ@`)nH1F+Kk?Arp2?!*=yo#M)kCuv-|MpZcm zMois?SXUrgcfw4#@~m!Iht`oyxF!|;1NT$^!T%vMs_0iS;b`Q>tg1gMMA&MMNh4E# zFp`Av5nR1U=A1Pv>1jdR=lgwZU)k3(;acVRR{iUbAv+>z{Fh#H%1|i5`yCnrjG(KR z2;wrQz!jn0Ewyt^TKxb<-dJ~d>^np+68`;S|5(Q{@DH5)2mhD!);m-j^Gzt++ErK; z5h2R2>;14wkmp0LD(kmBE_*Ey7V1PY;li`HrThN{51vjWhQIB+&h-&tqc{)V-%rIk zAQP#U@3c3#h}Bf+)tiIu1Uu+-UB>EhDU$eq5`&ZwJcicTiv!DdLQsy#=^x$$=6Z}w zxJ{H0B4T|~QI5<(wOx_WU=zUHVd98ybGe-QX!aOipf;EDI6k8+dvTxmsO4Liub_SQ z;=Ew6ewt|P7+G(-j8?2DXtmYG%7=!HCe8z1-0|gfX4Y6e{&!c}yR|scQ#&e0S@?!7 zn!BbL`e!+onRlh z1U#2R5QYlI_X_D-#^;>J3}z^bTYs;Z!iyX8)$Wjk=xK*%DTimVhl%ikZ5r?mS;r;- z;D4?x8D>g}Ii*E8rQ<+`{gtUky#$5>B@508RAg4(Un_v4Cbr^-heQV(R@Ll_sIhVa zE06hW`-|F7yHE2+qm&aBJWbnw!ky^b*jv*Kpd zsf;z1FH46qoz%&;;dhu*nNhcc?LZ6ezWQR}Khcg-|2JG&6@AlXz)Geyw)VR(fqyAg z%%Fp!kVJGJp-~IYIdZ~wSq=n6x9vj(fwe=H!>vOFZVEwxwXh<766*id7tYj~e-jYC zW&U-x2`=KN^umi}7roJwvnRy1{wVZ9SE?+QW94JE{_jk6-jzGlgTP375^eT(@x2Zu zl~t*})sy-R(R4t3apM;5P$5+nkIvb2fdGh(+f*$~EJ6Wp7RC634~q*ND@^LV-X++2 z=^cNBmLrW4@nnMc-XO!zy=Gi5?ye~gdiLW{4nNuSpZkRC6H424gD9V#B^-RyeL4hE zIz6Jz4}{d4Vn)Kr-(V&URE~jiwY*n%`?F6P(A;2?HvY!O>8~iII62pb=BPzyMxg zFwuxnYMnhLg2j|RfRz&RP#P#sq!m>|*nr}}CNmF+AmZUoBBj9|ou3*xk;Qz8<0kv2 zRjvJMk~SG_8X#dgJ5JlL0A)whOU|%6j+$Kvahctc!zunYxBJU^dkU-{55`aFlLs&-ynm%A}L8`tez#)=NPW*2g ztv-Q=WP;%gili_=H~M?pHLBmPMySTFEx9pdAnQf7+n}S=Lx z+nn$&7bD2(iC9;VPciImO>07=&w-167F>$^Wt>lOTMfFZZn1o2UI>}`NgvKh-$@;M z(~ywvjHK;aa~nQ1`|H=~nW}_j!`V`l^gT9f@M!h%e4g4ZjQCZ=YtVb?&C-YEKr~$n z5ZOF;_}f~d#FMV7=1V^%)}qrbBlx6ztc?Gx^@1mKhaR?4EH&JvCKc) zug7WxU+%>l+LrLG#w5}x(*^v7-?uqeh!}j>e7atO?y~`0F zpyLBFbjsy6r)fEK9Yp3iE_69#UNKpX?v?4Y1bb`fwj}wv7d}(@I(d94RCXy;XDJj~ zxD<+Mb!&LZNAx9nX-KGz$COOX=-eIj(anS`1r|m-T4_)SJYy@y{-Zn62ly1(LkCsz zn02BdU6Pcc1jq5`?H8&I3cZ~l#qzg?S#rG(a#}@3)?hrj5uveup)r!ToOSBQmB<%k zvcw$Aq8!WJU?20@)o5)-pD%J>IJHh(ij1ewGLA`r+%y6z7m*SKQ7nWlq(&UQ<`jb1 zd9k2jHbTQUCukZm4^!gHf7(-HSO`5{jHiFj22A~2kRj8S%;s>0c|;4iwwWy38P zDJKEjhY|7#MT{wwAcO@)da|Fz1W=12_K#yo(905Ji1?rOy)P(YnXj4z+ljHY$9%Ii z0FK=FoYTl})-DNRrCwLJ&rpM8UN%^w2OOc7bqdfIKY3Wp(m8l##zB_spVmmIr9n3w zcqHYLq>7CbzmhiWz)AW3&z#4N4^fN`-L$?C{a(8hm@X|nnL#^C>(3A>%C4HbZEirz zPlF;3|Aewp3a!g@i|Lr(k?h9RIwj!5+|%HnbmHuv86 zVH_sDnY)YkGhqK=yk`bt@MD9xqSyhpi+2;vAY_A>v5GbS^+OkLNBbap@-C<4Q^>-T z=>_@&n25HESJxwN&<;&~wb_4zm?aGVibzKQPD3ClY=a_y%bYVha$_lAgCRYVLeR#^ zS2dW5`~i^Cn;P8~!fi=`c4aZ@ zaiuLdCa?|N;YKJ+IlD}M28|nx*wH}@6sMF{S0CgXH;D%3_@#e-qm_>;J}1)H=eAAX zXx8(EylrAb&>(9U>m^4Qt7F!NZuH_qlr;AC{AHs=;nQGuuU&|r;uF=&Rr)r!<`#F# z6_LO;_xvtrAuwIxJe|(dz5Q!A|7ALk8`?)d21&U=J384Px}U-)?&Sw23G{Zkx$HdA z24K6S-&Z?;W^HX(OyBl9)i7RHjUxr|BH60rJiQJBN?hnCdLiAd;kEmy3PfFgB;Aj^ zT_rS{{Ir@8ZvaJ&A5~3uR)Fl=tTH~KVYRs7JD0Oy@>T!pj$rI3Dn$$SGVw7q)-l7B zK9>DQ>=0fQC)W(@KH`4>!5+(4s^Tb1s3F?_Aq3dRXum6LC@rGOHq=*6ufT-{p}E*2 zwQozJ0-a8^}+%ZSaI%SEa#?Yv*p9=arZ2V8( z{}Lf#c$gaYe_))F=Ib zl%>^_y(JW;qByJa)tMHfId$^{Hi=opo(_Uo^fSmcbhG)%PDXH^s^`-MRsaMIapFit z#hCPk?(iEH6=Xy<0P>bj4{{$Ukx}5NKhT@bKM^Cqx5i`rK2n!mg&T@m#UJl-Eep|= zvA34CKlx^VLMCS)jR;;tnt*X@@!upqPkh@vwB}J%xc%?KdCX$=(Ole*qawVH0ZyJy zd1OrKMDvKz+StDbgm<8%1#tWJ8+n91yqiqi7{3EMqV?tMbzd;{qM{uG@~|!3>hV=1 z>~%%$@gC!^>qn6kKCIBWef+OFeEev{l(Rihw6CNpO?bJF<7b`X`&f2 zmA0wN{aHKW_z+(QZogJXS;BsSh#-TU$3Anj8>YvfBp}`tQhmfcjEF`BhkzdtxPjM` zgWQwz1T&4EfE=|T zSk7$z`TyOna5=BRlF?b$LknTJ>8i1@PjQ>YTgDQ7Zfc}S(hb0ZRc6&sO!P0L5(1I#1Q#sZ zhW&NAq+c@oru%+|zVVsIB<#r{D1?_ zi$l=LzCWcf7#1is6A4p~qcl`baxolG_}mJPIgWOBlRf~`O%3!;R*B0(clJMK7l7Xl z(E@W3xhr+oZ5HqUXnF)WDMG!fFuLtfj zeoXVA)t(V&s{&nMP}L_01U=B>B7Xi@pD!MrgvHQsece3m8B)1W($M^Yk>p(t(Ui)7 z>5WMpp+Q&@SZ}_`ORc~>Os4)Dwst8}2T8rjAmiBnY?2p_m6N#aBfq#Tg1b3BBgt%5 zavr5B;MLSKo$aL8mtI?DgDbk2LVA zMVd|dM^u(pv0Kg0FeHgaRJJ~w^09F$t~8r6QJCB%DCu^3idDPxed-W>Ys(kyl|Nc* z%_xkgf6Fs-3;HtVt57v#Ic?&tSwe*pPZx>`E2O65D%`Q?xu&tA`ST}*2WxTVJWvwM zk*Mn7+`h>|+Yu+Oa#0x7{{7v~<_00!&7Z9ic!VRLuNm=V6AN`qLW%52^lckAQ@vf1F9%my6(Wka&TmF?oK z?~k8y$0Ahx+7>OB8Fc$a@hd-i(7!}FUjlW`1qH_&dzwv|88rA`;VA6qH}y*jbq-_v z)Km3gdz?P~G`Z$s0_NN>*C5{c;C=k+%o^XYf{BFpKc2+C7BI-GnvhR^QPVC<+Z2 zzqS&U_XH$OIsSCi6rDuJD`=?TBfdrrWrC-kO?sRQ5Twr>_o1jpqV z%4izDvS)p~$pjPj_WAFiJssfK0=Xpjo zfG}2#?Aiq~nqoxNAq&-SX(Up4&fA)#moUpqurlG`GeS8LaK)J`VQUA(?B6DWx(O2l z44R%XbhQvnBKXMvGw-$tqlUD|SY0UNg~j4bxd-TxGDdQ-cuNncPdTyBc3D5oN*JM;OA1VpS<@sM%L-y2#5~{tpN-MD0s^s7J9P zSYY`tG0xtX_I}|&;a5*K$X@D{AKOofN?V-^_y_{3Z9?O4;3HI6F0ee5hOF-2yQKGX) zcs*9MNB=vqk3)&ZM|*G~=242@ol|+(KG;7QT^D{QV35Z(V-v0%ODA&0nf1 zu}z@>t)NukuO7NF5z4V)&y?6zLy5m3fEF}%Hgxt&xfK5^LwK}al#@3ROy8Rb&y*aA zy*dbR-`I-+>_yozgpYm$*7#Jb!PtiIbcXPSEU6zn(&nA)wZ#ey5k$aFtV5Kv_1I$H9(9Ni4&YU{AB9bXkNPcwX@Oc@-pBqfSU)=z9$@nW*WexCb6qF~W0~~pSh@LBRP?jxL>O}2b>F(Mma{!bD#ZKkoTkSH(D*oR)6xlfko0AD0%)!6 zB#_(EV|zW>Rff601hc=vhjFQ`@9Zi|%aJ%Le)TJcu(jh-pWd9LH-2>`5{E85_Ul_u zVjBrhjKFAP&G{=~edB%-W6d{`qOAk;*4zT19rNlCZ3NH)P31*g{*680%s#`=nvfp5 z-438Nc@w?8owsM2-)9Ox5>xXh5~q$p*;XQa)->OJXj}^YJ@#*OIW3ejlzEGxNkjby zfB6Bi*iFYuo z!i+)cD`N^QvM|v;F|q3 zjOVbV7`mC{Y#y!l&?%Yn*DGNlStgo;Gite0QuBhMx#dhb5;jGbI|)i^$X9_gYEi%= zPd~u_*UK3rZPVKvoV)ZAKxK?`Oz2qQT#VVqrMaekOn8u>E_6RQV@l=fFc=8~fMtU> zK^Z3a#kzS)pp-6QVH3%%@0?$Px`W!#@kL1;S}Tz2JW1@$b8mmXwb|Db8aR2{Qxua^ zRM6=X@-2{riz4H&#HQUUYWk&^YZCOl3GyW8%(p^_O-}XK&6=(L8590j%nWl+Hrg+> zXrn|d_V7M=_xzXBBcnLq3yAVLDVOVoaz`HG4LAEa&SAXo$(e^6^-Ys_f%UvLcu&@= zRNENOu;>~`2jGYccc4FHd!byjdm0U=k5!Fka^ZRb1rv{i5u=`Q&sP0Cj&gXS4=wyy zI?#B^zj_3(P2b`6o{+$FW`5Mqnz$r7lpFo5%Evu|e3k3k#7nU-*+irPuj9QHECKrJ zcltvk{>aGI$a)Av7HC+2@#9*woo#=ghAAZ*8Q(9I?J*g!o43QgUTEo9d44U$_xfV( z*%a;$2DY$=`-0j-4m{G+2npWSlX##Az4#pv=5<)K>i-(hFHZWO zKZKI`e%x9s(mEN|J)!vK?5>pS&f*9CWlq#WZbTGQXvI3zrJ@I?2=QDUfyY*yhzPzn z_Qj-yFDx=Kj-dt!591`KH_~ZVBG+Xw==z!_`Zn<-M3v<#C;qW~T4l&HcZZm^x^Y0v(#122kKA@T_nE=WxkLgW&uz^JXxz_%t{q~vCiURFULq9-VX4yEsk zGP{3z+27dCI$Xe2y7;CqKEY~x4tLd!-ku|cs5iXVj1&XS(qG3y0u`_ zC0Ea|j5nqLod_1ISHA8&_t#GHiqkh(iA!mvoxKygZJ%fFO(T+>XN^^RY!L_uI)i7i| z3tz2%kPTgLD5O-WJVOoYT&zuOAYHvw_gfH}%fQ;npN*>ylt4TH67enG{2(_mIPQyh zeXYAqsZ;oH%^J%s2AXxyBQ=o_gP% z-Sj;Cttw)PSu`=bLYm_}gCrt$oqrN}X9+SJQ61wo{$=6+8y$xP<}*^w1%~Nqig5I| z*yRocr!``7HRFb!XKFtl(QkUQAHJB3CH#i-N6r2j{-eB}HKF5V3uO{A*Z0YnhaVlm zh69Thy5LpvI5AlC1xA2wmk5;eE2H81X!7X3ra=NJf-wzV%{&3UmwwuVh3WdMI=zss z;=G%OXe_5#YU!weTC!IOpKZ|*uQ?sz0Di%d)qP`PscI%OvmGmZ^Dnj_HUotXBa^ca zG3!QSsMg8>NW|l2e+uB1M|;1>{L1q;vFhc+82+gSvvCqi&u|Y>xp~(3v~NR7*NING zf#683wqf>xx!$`<>Juve9O9`MeFdrwKBtr1lMGS*f6IJT9M;q z2UvWo-b8dEdJXJtj(Q)e!Roj7$lZ*x_oz|#fY$P&m3*P*;1g=|MJJ~f!}-``)vH3= zxp6j0*Q)P^b8G+nur6bgxpF^wbw7E$t;+!VdAV2nJ|Di+WB>GWbPHIs`Xb&uc=t62 z_EdfYaHa#AY8))qcdaaopIK}o>Q%xf_ddhrI3Oe^lWh6?HY=0BaqLEXb=p-e&X`~? oR)cy!F=%^c)Kqp*40)BFE0mcY!tSc>ctu}4v=m))hJE+{0A4=B!~g&Q literal 16134 zcmZvC1ymeOw`~##7TkRT1RLDlEx0?u-QC>=cbDJ_RabY`q|(wuKSvxW6!tOA-upbvyS49N>A;T?t`We`M4WqcLh zW$NDy1Wm$U7e6;XKRmX2JzxL2xAS{`d3jsI;H@2^_kMU>j3wcJ2V?jd%3mx!;rcy9 zen^%BS4w~}ood~Bq^dmor>SAKCj>w&Md!|4yzge*E1B=teshPSmjwK-Q|F-@Z+F4+ z7jsvU?!9}dfH{*e(9qf3b8L=CPG^74<`x4`+$`TMio_GH4rdkbCeVZWv)ReSTvuoK zxj-j;*UQsmR~uMfK+hNV{r%Tj>ctpF`^%MqC3xs;4eWRR#^dds6Z3K&+ZA$asd0b! z*tNLfcXJZX_aats+?MMJLmxWHU9Ql|&wOfp5Xf?kMQbx9zP3oJi% z{&s5f0J%v^w63WFzreR=;EOvaPl`Pk=Q9D{v-Kia=9i1JSFm%Q#t$6Z>Mwx7_R*=Q zxmkkzu_}YN?mdeUO2xZRyd!07tv0g!I-QkGJ|$&#<)_W6MX0Tg!YI_gpMMG4Z8vgUKd`Mv&1NHxe~%u` z|879ZhguNGM%^3!A+IyN<8o+C+w0YYnx+B9DE&kDrwZr;atR{U4Q&!PdaI)X9$gLR zY@7hD(~w9DPA8H;*M$;u(tGP)T`_=5B8FxtGv|n%yu?|zQ6{Wa)aAUPgNGyGC-8{%$V?!?mIyxf@%#|yXVBJ=(6V=H+7qbNZ^Nao zkKZyX%Ozj^kcpd|TSi!hODAc12<-QKKh@Roe)DK{|MCc)0_42DYvbz}{(bO2dKmom zkm6U-q0w=traYGunuo^!_Vb$!x^}^C-=UEJZvc31%I`K1CBNY@+8`+!jUOr8qk>%9 z{+i*ieEXN5T51Uejn)&(Tu18U%Mkac^$4$`T1aD$`mXx-84SQ{$rq!x zY08J8zhklQBjwfY1M)R?)j#dbcJ5! zvRI0oxG!&^>G-HA#$j?RoCDv_j?04Pej|0uCQM87mY)PM#Iu#?&Ir#GQ_QAJF-qoF)Hc(LXsw+C0 zM^eQxr;(h)$``r>ps3G6AFLvH^X(v=kPjmprbDQ}!#;&l7F{^DxEa|9fNQxv>Y>X( z<7)frckpq8p62ZW_Qg>Xjh7-EPi55B*=)|w#D8h|8-tSgSetBbqepk_jepk>?6?Rz za9TT-`6dCLLWfZt+Adn1YE>wo0ni+qNxb&HT5zp%r{%wu6)qPPU6ttRZcQucH~317 z7>|dT2fCNwTEOH^3{%7INTybjveT5>nsG$>{kOhd%XpgX1qxsw^%_SL^y8pmUxwx< zGdXL7W)PKP=i}|`uc^1!_P5sI5AsXWJ9!D;pW0xBH=KI7a7&||fZR|dBjoha2>~7e zGg5Hx%KbZ26PxqPUIgDUf7knC^VZW6j9jPJyGMTC+Oyl%+y#468)@h7`~c+lJN60{ zweCJWo!C+CEkndj<3FR4g%A-Cu*G-uva}BKIjL>zc>* z!>>>39ug;Xsg0icHUN!*XtQ#ILCU zaKO89&UE#vU1Qi*_Y?Lsy?D@1GdtJ`M<&1L<9FHDWSBRR<)GDtA8@qCBK{|?vt~lZ zCpx?i%B!eh`8adwxd$0HRx{DvW%WC95-~#yKV@>twFet%K-!}*X4xaMGnw)_SfB+K zQ`sQGb?9MlICTlX3|)iNjqWx|<7JF11AZfLd+h6V``IbR_7lsZSmMCOHEdXgum5m8 zY#4KU-Bvx2%yL9)6fOMdT;R37jfl_|wzg9`>%4BpY==pK$0yXWt@AKq?$&Ubi!=A} z)T5kd1~%GSK&xqqdmYzpr?vtpX2&ffu-ldCEEN0Rfhx=5_V1lkIN-Z@z%3nOO-><{GMCOXrzc}%PDC|tW-{; zF}OU-2lU1a-A{eP<&h2X^vqHdZiYRB6p%}ILB?uNNpiX#-09Evdk*h$&viGutsYcT z%_q}W_Qm6r=`+d|Rl*TR!u4BZ4qoXRoX^hm)Pr+$eVP#R`{6eyn zSZgA)%%goh>U)<7xFK`@bk_SQcHFKg(KeIA<60~;LV!BO!bq2+@ZsooR-)Z)Z{{1O zgmq?cu!ly@=mV8++1Ufg`HZavUOAh_uEk4zUF@=P&n(4H;Mqxy*#uuV+Jxf|6@r5D zd|2St&nCI(?5BnbpWk%psG1sT(RH85i|-P{$t82LWw1g_g8U{X|G1kK+jA?|ncrU6 zkGYIV$A=8R1X}L8T7I$vrdQHdVI5md@Mc?*c(Y|wYhvg+RK9D#CW8fDoveOHsgtdZ zgBD`bw#JqZI0hsm$5`eB(*$xGrh0ESBD!MT?z>WW6w0+f?)|FJB9BcVM=XnAY*$A9Gv$xiIp}gkFy0N+lastEY+m3;S_-=)}>8sY{(^%02fIROUQV z=6vGBQPROux##cGrAE(LO_f>8E_K!Yt;ULux)dCg9AsABLtCAhLqAOwsjd_QvCL9u z$yhV$dLG5x@k8{M=#zSW?%#q3NO{;D2NO{jh@2xI|+J(J%_B4$q z8KFc!YKT;voS$iw_IB{#gDij05c?_xHtDl`=_mNoE+QV{s!J}tn&A)<4)mG z1;TwrCdk~S+|^2^X8FyeT6A@@jk6V@&EMqjP9`MZei}BwC9YuF{n+*nc^ToyJZEXb z9w5LTpp4wUNUFOXde*>Xpo^%+9{3Wu-6(cBkne7w*a6ur6gwJ9vR;ey>R1-A2XG>{ zL&Ppa#V&tDN*Vk#!yd4T+-?=S{G0z^toRc1-v*1sg!*#z>nN!v;PFMU_QTT?>BOc2 zxG<6#dxs}iVtByGi?}MzA4gJ#AyHLNZsG-QjZG-P6mkkSm~Fcl-{q6Dm_F8R) zru1~^K}}{=Dw-K7`urW{pKv$!@420YQSgcSeM)%Fr9SMr`!!0g*j?XW-PFZ6_@5Y3 ztdYRuE>On2Nyux~am2<1hGoOV$&zK2L{{c~StfwQO5Sgm1^77&Q_jMimYb4K-n%9BMkLgj&Xh#8O`Lhyn8F zx^7it|FUzw^Rz~B^N(m6JU=JE1g47C>(CTIbpmt(eAd=+9M*BE?88&m7fYd&HZ@$1 z05FrU1VO)}{^+wHu}8jB%Fc9&uS> z^>%hn%oS6;CKnp^=AO3M#LN+xiC623{+dnCKA?3?W7waLQCu0j&rxRMH~IAe)RT>; z4NwyejD$jCuE@=+679(Pa8}K#$QP|rzcjfNLPw4i?sPO&xflnPuRiR49EKuv|3E{8 zyZe`mTEQ!NHn2u!iHc_*k(E!-ilU&xj9G1AxEV_UM^R_7e_YAq*tE)tPTOr(<*#bN z^aY{`IWdT3%HDbz{4>u&KDK^uZHDC}Vpj-Tk0xOYJHCT8m*#ht7mQOy7P#1D3lD$b zP~?Z+3QM=xNtLNa<0smC#HKsMyS|FVb1+`a1W^^oeJ=}ZC{RWOtG_?9P+?p;Pb5br zP|8-wMcfF?4e*+4cG@h{NSM`^3Zh2hmkCmh^D$GZ5HsV>>?BdXvT8-j-w`49HZ(Pg zXHLh1#ByHxA-`a3;7VsIVv%VNL3lRf_-&P$sonf9*W$~T-ERt0LOq_7A95D4aLJvj z+}xQ!hTh(q;Aj>y{Cp1$J^wy&wqu`pUf+T&e=Xt(26tTlHfO9y!%wFkJbT zoM?KC_>syKuA71-0H)qQL9-jLo>MXOSLcf;{rXg@$Ox^z3AO^`my-0)wBw%;Og}~w ze#sdBBxU-MtKNTnOn8D;-{2qJ+#P+%1Us(7Amv?fg7&K!wgStSw6xEw@tR?wLD-2w z*yQ!7NU(Giuyj(UB={n#GLUUNP-Mz`lVrJIuI&pti2Sj=1n+NNuE%03hg07Wd1SCR zu2W-rMN1VGJHThSz-DK6-$7i00~SG>n}1mC6KC>!bBhCKBlQl8Cn~ zBktM+-R^9U1_fdB9akR{5?UNqTacU!c2;28mI3Ua*7gXz0?xKsBL$mp3)G>xJ$!N# zDFft)q1&umi*8!mx{T2dRIm^J;2->H#yW5&n@-NcxY5kDdRiJk_2Y*n3?h<3(|<{6q|CL}G7g~EYg7trv#4c7^2oJ<4P6tYlz8v- zZru+SPMOI=P5k`%L)`sXDod+z=1CEnV! z$7C?5lRy$4G%WFIjZQI58flHTeG^+v$aKq1QX=0=dL@jS`=oVNLbY1~wy~rJ zWDjhvfgPl)#IkftzBi1kXEv^!#5561M{huO9>P)56nm=$d#lb$dnt;>@!vD~!{Zx5E}+QR?5aEAODA#d=LdGBs6RmdD&}8-#mrm^BE%mw{&9 zTEs7sXF4^T?psW)ImDkWV*tiZFZwJ)DELkedur^=@ppyEx$3gcb|3}M0;}j3q^TIE7rAXm;?vqZ zYzL)CjmgWtL4^T}64LSVwL9GmeLAxQ9^yHXc{ylMwz19^Wtlbe&_Y_^d8n}xbRpb# zv^dhQVuBI=m_3V?aHw7;$)N{n7{WXY5>bOfNkW&X-YM@K``SW8o?sD=VZg^L{FwXs z?hD{msIP1=`P&H9W_hWDVy)YAl*TD{q?$kO=zO@%^9HA@PgFkdNyMrF`y@iy>FKrO~!cQh}=dHPzv ziWe^W4=rMES#YK5BLG$G$Wj;kKUWfaR}u?X5^`4(>lA)6k5?VK=;-6LemD2jesY$B zF?&)uxLVSxD6?v#VrTI&l}ioBbsOw%9e<^Af4IDy-U z3(48>tRd{MQtI7|D^RLzpQj?(wT7zf8Y}G;2T;~p~3 z8Wi?@2gM_k5s7o3ND-Oln^JeTn17nntwHU8BTfsQl*&6{I_?GD(35)}OYEZF*4xuA zc9zZi)3Pq09NzFdA^Xw1@vm!Abk&`%sXc}iby(RwB~lkVs4w$d)CngOCV!y(k(Tqp zawIvY^m0>>p?WO=wL{!7yMl!OD5q(fF2d{{5Lg*fRT^BS*_nCUKpkT1g>`ita<*J7 zy!d4eL+Bcq$J2k8^?Lpb#bXIztgwft4_pe)3_in(WHy%0@QW3`cb@XZn3aC;W2KkfZ>Ty!rz7nbXYqX5b>ZkZ!~nd9H70@&&Xg9T2z76agN`UN+Y zJ^LMBOQ!#hz}5E+Op`ivlQH7%V+oa_D0$0X1QS}fq}o;Bj>}(};zi@qs7%%i8N8f> zWrC#3%Rqew^}(iD(h5&F91|VufIe41Zw;e*X_QS-l)7s6Z3A7hLp|~-wuyJXnVrHQ zrS@@$6rNEl5bx~XQrC?1h#P}xKD`i%gW5>7x6(7`v^LkGZ2pNq`7*qXPh}9ieTy~v zV9b<8knGUYAYPPu7#ljf0^G@~E65@=4ogp3qMAC#!osCLG3)V2ny6bB{Pk|A?! zpb@9Sph=$Qnw|ocQ9QL#Ezs!FhT6!Q%7_+#`jdLc$i%BED%N6yD7lt?uT(QOO&D+S zc1zN6@=66~v<03lbF`(RA<3$!h>FeXhXr-2)Y!KSCzI8SZ{}{vOy4du8#}a7?UQcXVME;kQ1;_VB0x85wwrv+cK=)Gx~) z6cSC77OlipOK=_$Ca9_v7{I_c89`*L-W1@Q=f}rBF~KI4jfd?ICmkQF*~-fUbvFvPFG-PbKpQ1JdciwxrQ1_#a-2$+l+x54asx(2 zFFTm!3aeGywMs>r{oS$#pGHF?hMFRVe6ajjbIg^3iy}6{`e{@;+H?oXF|ewURlL<~ zLNZ-~6|sQ2WABQ>gvO$s zI6!BhS@i5%QDWSLN{96W-iS6(H=^$Fwz3@;>!3{GxY)sh`@WH<%uRiuT(N^*uc|dh zrRb(o<%QMF_0R8nrAwp$8p;3~m(pzl1T{GXwG5?!f8Y8B9IPqLsc&YT_v|pXnm9H9 zK}l9V%j1h8NVk%rbQw;K4e8Q^M-IryovtSJ^a_j@it(3+(ieX7KXcBt>3w_V#Om}T z;DEp3`Ia1EGP0ptZP>V~q1wgKL$KRy z0svze>)Myx0uo@}!;^J$Q`r&&F;j-H{k%`V2eDeu1Z4 z9)dsPo8phbyCABM^)^RL@aD^pI4K~R1Y-(fL%OQSQ6GDC8=|A97pBNnJ=$jL>ERR4 z>i*M*b^b~BE{{In>#eTLBgwGHxVjGI*G3NNSRWh7RVkDMDP!|lsObnw*B76=Z@jImvpnhgaQ;@SusyO_i?}Wy1#7ox_^`fybOJl>_tCM zA&^b)_nZrv(|XSuL0^g3Uo^ug2$;8!->1}l#^0x1Y$0Lb9%1Vg)OGI28>aJ6bP|a* znccw|jVvoAG~`JZQBmgVe^WtLl;1<;fk0Ov$Xs?0bx$S6HNq(chbT32BLOG-l*U^=$*be^nK=0)nW1IiAqodidx%E3G?8>pJV4T(@!%AiSh2!k5iP^`$9ETH239s}aMz%AEk+#@z*cu4Zf$(;aKKxV9B>5+A z=BR@b!0#sx+i+0Ua8L(WCFXTk6kC}qCK02BoJ$iQ($^AiAjohCZ*0|>DY@XsdP62o zPnvN>y4adjyxSjlIaznPH3#63B#g3-o=8ubWKWqR@IMcfO@7bcxli{-?Mo#uXR&hJ z{!i*jL}z?0G5s+lg(i_@WD}mGQ-!8_cCmlp)Iaz?q_@ekoS7GO`a(dSG6K{cD(j$u zEG4y}ljJYy0bEn1AV;E67plcP9gt)8t8NkG@UL7Ga~HqrKXf~oTZmxGs6qIP=``hM zLp0L+15dC9>%`&f*y$(i5W91#*Ss6hEI`VS>Qyr{9|CjC{=xqtJF9Mn3V%_3^fLW@ zm{0~~mESM-QTcb$f%c(%n+H9w?DjwB{=c30pP+MHXUNDn@H2Jc0jZRJ@8M>PN9?@EF)o6`g_Bah=p)o|G%8Ev5mPuTc+#G`NLEnYA#3CXK*LfOXTdS8RMHKR^K z5s!?S>KGD*vMXio79G0cNQ2ruP3i#jG>MJORKF*37m$98iH%($9y!m{slm9^DJ0M%z-40;)I^^7z|T^WD7r@##Jya)195v@ zM;-3I+#w>AMF|?;ld$6jm>VlhPv+_i1aV8*;y=n5-PY1DmlPnmH39g>b1%LI0o_PS zpT9&RN}1v%>99~e+L$Pm#S4{QeJq7szxztUHKb%nl0Vi!S5=vk3*ns%nlI1`=AhP>;~ICB=66`9L6Z=3V@_Yp(ZE&ou?M6mEs z&WVO~%_94ZH3`fGn)#q!xA`VMO&5`t6Wzrdgn0^EMJt3hR&-mYsW*T+ zAvL|s6LjEJzT@CA6>90PEW922GEvX``?t*NeMh)+)z&GZDZkY?>Xp0-m}6k*IOs7m z)n>=k<$NdGB?)LGa3d%`Sw=1H5fDREsI~#Z+e*Jtd8cIX2 z7h;{Er!fAttsZ&RqkP6$nl7)y;y}uWcRFyK1u53>IO9l_D$;2WX`_P#kNpL4RLppT z$V8v4a2r!8@ulmdN!E8TgFmwz^c@n_j;O33UJ^-phZz03-76e}V(9Lp*8m#D@e%->R|M5^Gu7Unc^5tkK6LY(#1pbYc=sFa_b^7k_dd3Z;*}X>TGmZ`+d)wr3@`R28s${p z;>br-EjpFjv*WU~DEotLLbWW4x0AC%wR08Cmz1{)W1{oc0LMdKEr=(j7tI_ROPm)q zcF8`fpqVW4q_d{SErB;$K?V6u7sfjrvV%9FY8S)n+qi-?mRAV14VLEn9XNYJXmSv` zI`3*VNRQ=t5*|tBkd}#$w8M| z%p`%=wk64WmWNoGGoy>h-l#gFQT=E0%^BoX-0~ctTj$=;P#asLeFlp!Gi(XeK$JDv+IX}PKIX?rK--D79 zUoX*T_{c4J`GNmgfx!T973^b8U!)JP%v?14NRi!P3b?X85mCpntUET}0wFz5V?9p~ zo%9jcqGaC2ud&;n5AfF{D74(sq?jzVQ1=ZMArg!+pSa$dC;AA^zZ?nV38Nd%y=)7? z(kIl%?h_37+>s2Cj_s{D&c%%{!!Dda3DADd@S}a^G(d4P15oyF!`wLtQ*?fK<|M&h ztdC9nJI>J04-}<3t~>0Csa{05tJPzt%QFRdgM2RNo`*4aGUBfjd{}9urj~}_Yg+<* zSOdC8k#)!U%e3${7iVQo$ee;5yHdoR7Z=JKW(87iYk`1dSfPG1`Ecrzj;NM+qp~Vvs`4f?icppM2q!wax zNM$CK304)P9M^+Q67FA$qNXwpvL z;tM3w5CSd_O_(fL94;Cap9JDC<`OpFeT)?&V=6n~iJIgw%Kk$d{8hEOP42GeZoc6S z2-sRS|B5Tj7_2|MhuVW0Nb;Bt7g`~bq7U~^0xbd;ii$|`Z`~2%xdwa@={668>$%mH z45u!HJAWdU5iIgN*y!+ie_M2k8SfT{tOV+E(_9|jxDxzkY#St8HOQD7W(bdD9em4+ zon0aEQ?6+uZsGiVG^HY7hwb?8F}l>DTlHnIGk7Bn!?(UQDR84u>w0BL>Rq9BpLv-0~cjZ(jdmTwb949?#ml5f6a-BJWzUv~=$}#wtU}rZPR`hb{ zDiedk!Oqu7oVg0jK`9;U_tDp>DSr^@Wj~n58xMjz2IJn;U-pmo*nC@Pt7o=3TJ|`~ z{ixK}haV>nM+xYBo$CJn%P!fGwvl#3vUEfu^Fl#}WLEBg`7)^TV!CDw`5G%nEEEukS+ea^6W?F7J)UK3E?M99X{gxw^Io|EDc@dB4hm17%>~u#! zArjs>FZ;$=*CM`79Tkr>kFrKDdM~2>n9jm}TN9vA^Z^3o2dwoacK3CUF%~j?WIDDfJ&_(S_hW{d-^dg>h znYn+3uUr7GS0K=ddZ!vhKtSRiZLs2KX+MF!PgDhAp+osUQCp$Jx$6&ghm;Smq2(itI->2q1|kW-E0b1nW2Gf ziGghSyByJZmc@CN_J6gB^25-$54~%m;E#ijD(57*F7z37dhAA%nrgI2B1E8_;Pz3+ z)4PNjLHd(C8*rQ3JslJo4QC5i62e6eXVoqM zdb37yLn@FmN{|!@^4YJ|!~UW+ayiS1+WZ4ZEJgm9a?$;x{Fk_v`BR+Fu1`8T95htL zF(ZCj5DCn8`e+z?68D!?{O4E0M4yPT3C}!H>#!x%S`tH%{^AE7w9Fz<_@C{^lj82_81mXWBitg-$(9i>)WbwueAAM^SZC&u6n;HGRm#^rXHc&!*cl_=8V+r|cY`;!)*nJb%ii{X9fp+C?= zGSEXWJ<#B&+|}&OEc;XfxJh`u$4}7U;PzEPd$~K7CuV4{wNpVCa#F!JPIWumn?4h# z0_>i6?ZEmckmE){)@Ih3*B??&%GEuXK&QIJnMn8;IzVsTjH0By3dQNMwo`M+Km`{w3>TvTAM?-zhs+L# zoPq*31vkkQz(vU^dv?i*k-&qV+>HN{b28diG&CrkbD1Lu_gV$^Q3m#%f47gRMbwEkK?t0~Ei=V0 z6W4`{fzRg1HL@e3Ai&UpxNi^zb|CY>n^xveD7=0;-C z=a!uX{->VkbF(Ky`Tg^#aJ7-03Xc#%3h?Gav zHSFa7L$uN?hm#=eG^%a#fn_A-?msLY>u0kp{9xNVcBjBWBPQh)bq~8h-6H7~2?oKT z{BPoCJ38@3X&5Q@NHSu#!hpV_1xav{{#J`Ccsjl^@(FdDq+cWqgo;8!EX*714tM$g zAzEp+5Aiq@xk~Bm&Ac|e!e^f3Mt8ex?52v%kYY4;Ew(;j)v+3Vpu_qzqb=8H_?Q`V;=Cfq`y1IEcaDaJuJWgrXisG87&q0a znc2gtBWZ#*OJ5{;D6P?Od8_K%R*xU~MdHE2zavw2P0p{$e;B!lBOj#Kw8=dk8 zSxZT~q2URH=w5T}m!_dm zBRqwfw(;(!WyUk0s;QK%{WD$mhdhF5r9RVn<9ewMbh`QWvh(}0@fq|5b9l;zKj@yY z=9016X$-$A@2S*0#ifsU#H14Ui? zTOZ56HH38Op_EM4ICS9-pqst1d|R^osgAj-Z=KddMuKeLp(Y|U;efJOhfc7!}kqkO)p9MnjM0`;6P5LlX{0tA#Nd-m!t)CQB zYe=?T4Wo2yuP^I6iJ_L%m!Yht@-e?|vqUVUE-%kYqd|gXi-~f1o70sG}oBkqTp5Z zK+Yt&gjZpK{u2@A2a1&(FhW-c*0>C$UkEKqqtTP3Y^XN=`w z8~i$9tJx2Ovk~xwvwHYgG4h25-$nUzMF8SLH-gpX3S{*5(MlBFsvmL*ka_doJXt$; z5ZjQ8s9P}GBh5E9!GgUodVN{h=3AwnYSoWc8B1lFunlA3qECBTa!DwQ%5o~bd3AqF z0)m-)6-BW7_{Uogd~1qH>?gk2BPG@Bw-|@%=`pkR;^(#J=I@~WK0+&mC75w;I&TcC z;>n^?<2)vzqtFnk3Duu?!3t!9wnEOv=)wO7z%8IwXv#@L6r}$WyciXw`m&UsXqB)V zpmk^NQv4OK1*f?6vPrpQHkPu(p!YOqNsYjD$7bOw0ke-L_CJ<4!uL@pNHSRbLd=n8 zvP8h5tRM&=%;yqyN|{54C?fwQrbL~98DusaE+IuaPQW^!GJ{5}W( z3Gj?PNC(g=!XHxzv^@F?otW6+ZI9O_a`Oxx>qE3dMCK2{^Yu#GQcWBAjAz}8$l8l& z2g2(Fm_8V!ZLKi&jWPCB!?W1?qy;20LctnPsCU=EvnT}P4fi5e7{GK^GD1Z&LYbrm z)H6aMt%QuYZbkfyQBDi+3dN)9Lo_aD#W8?6VuX@T3m_dABpVlG85hJe{ffd87lK#P zhe&Gx1F3-||Eb-;wELH48k$QQTB{v)<^^L2p2H9$8NPwIjDdKPfjDb#R9bHoRbP}j zqAC-TDwDc;P&T%NCBsggXB0J{f!Y_ zPlBkpC5e&f1F{`_e2Wo^+meYWVfYYq1aeF%s-%}vVM%?y#Razx3B5>|W@#L{0dBR4RS0rLMalz%UT=(7DAoHvh!FA*5XkcXU6xo;Zb{QLr5bQB`OZGkot-5@`lqMh*q9& zLtNskOrgmTt!YIY;{F41*DVrY{$pN%W`&p?S(M`K#I;0IJz11$A&n217EWJ$t7*qO ztVtKTGf}h?2S(ujQx;ErA0Xl&>pwzP47z$j_CE2aum+2?4_JACqq-89}H<6OF@%J~DI=@Xl~bPreO z6RW>=57$`#!7j89o;^h;3O=S9F>lMe|n%$=|1U3kA-d%9nczwXll z-aF!bofh!l2}g?u97T77SB{gjTZ9UJ2Uo)sMQG#-NflW@lQ&1zIZ<4kj0G<3&| zo^$l?OcsS&`0K14U3Xj2sKK{BQ$2+N^z8?^%J|O!K`k{2Pegk7zSjzSA<3*M&@$NbmRd=&)sZq0jxUC5H+9f- zI1nM}15UddGp^K~31o5FRUWw&O?+bVFpt*AP6cbQ%iB3fGWUiYhG4IYG*F6AQ>4Z z=pbM9cj(VAg69c6xSP4i>xm`ax0BU|!HN2$Jq>6wf0?IH8|#q^Zz_U1aj?B_)Nsl0 zZ)v|&u_j&4!o9qFraMe`{nA_)X+I1zS3_l!(d)&poEQ08m0210lC{O1aM|hpCdo1&x+!6nZafEXK!6U=lDr??Q5$G z_67CyyMLT@Df;q!YV%!p*XM=HXEAo3+X;90&c$DR9Twvw%%$^kl);;>DJi8LeT_zk zZ_E7HJmSXV@@wbaoTJ@Z`>vdfjG=<`7}p)Y<1U{Wt`Q1MW#1CYid^;ORT+VGWj}wV zTc@8J5+&E;_t#nNov+=0CutaIsS;Pa^m{Ki-OmfJD>@o+P@)QG0QUziWpnrotX#hJ z8y3+g`clXz(mb+Oct~@j$GQ=^nhOKpiraL>Ek4!ftyu)wylQ&UmQ98e3p0>Q5&4Ue zabxLFV#!}}HhEf4X}@Ydqw*EsDC5Bde%bN({=-ZOh5JwTS-S1**1-F_rk9Mwkbi+G zFyfDPw-IPIswzg4NE*BlGqO*escl;3pLI^DYDdX-O2Ov5a=YgD2X@iTk0-<q?{$d~5ftF zvPDHxdBI5Uv7g9-CQjyxo^~&E%hY+Yg*dfS1`4{dM<$M09BoRnGtnUkr0tB3)3(q~_dJiEme!b%fwKm!_Ubyz^B5wR=Ew<5X(P#1G1_IY-n7Tcn#BaSJ}NU(|t11x0vLmLq)e8fdQq!su@iN>k#Qq z{q||ef&ysKHOXr4joNkC@UL05JES | Rremovepr (q) -> let td = remove_prop (find_pr th q) in add_meta th td meta + | Rremoveall -> + let it key _ = match (Mid.find key th.th_known).d_node with + | Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta + | _ -> () + in + Mid.iter it th.th_local | Rconverter (q,s,b) -> let cs = syntax_converter (find_ls th q) s b in add_meta th cs meta diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml index dc3c2fe31..a02e2e333 100644 --- a/src/driver/driver_ast.ml +++ b/src/driver/driver_ast.ml @@ -33,6 +33,7 @@ type th_rule = | Rsyntaxps of qualid * string * bool | Rconverter of qualid * string * bool | Rremovepr of qualid + | Rremoveall | Rmeta of string * metarg list type theory_rules = { diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll index d78521bc6..0e95e8f8c 100644 --- a/src/driver/driver_lexer.mll +++ b/src/driver/driver_lexer.mll @@ -47,6 +47,7 @@ "predicate", PREDICATE; "type", TYPE; "prop", PROP; + "allprops", ALL; "filename", FILENAME; "transformation", TRANSFORM; "plugin", PLUGIN; diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly index c722a9fde..8af74602c 100644 --- a/src/driver/driver_parser.mly +++ b/src/driver/driver_parser.mly @@ -28,7 +28,7 @@ %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF %token BLACKLIST %token MODULE EXCEPTION VAL CONVERTER -%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN +%token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN %token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT %token LEFTSQ RIGHTSQ LARROW @@ -90,6 +90,7 @@ trule: | syntax PREDICATE qualid STRING { Rsyntaxps ($3, $4, $1) } | syntax CONVERTER qualid STRING { Rconverter ($3, $4, $1) } | REMOVE PROP qualid { Rremovepr ($3) } +| REMOVE ALL { Rremoveall } | META ident meta_args { Rmeta ($2, $3) } | META STRING meta_args { Rmeta ($2, $3) } diff --git a/src/whyml/mlw_driver.ml b/src/whyml/mlw_driver.ml index 12ca5f578..40077d805 100644 --- a/src/whyml/mlw_driver.ml +++ b/src/whyml/mlw_driver.ml @@ -116,7 +116,13 @@ let load_driver env file extra_files = | Rconverter _ -> Loc.errorm "Syntax converter cannot be used in pure theories" | Rremovepr (q) -> - ignore (find_pr th q) + ignore (find_pr th q) + | Rremoveall -> + let it key _ = match (Mid.find key th.th_known).Decl.d_node with + | Decl.Dprop (_,symb,_) -> ignore symb + | _ -> () + in + Mid.iter it th.th_local | Rmeta (s,al) -> let rec ty_of_pty = function | PTyvar x -> -- GitLab