From 06e1fdc832d284497be5c62b980c5c7c6b0d7e6c Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Mon, 1 Oct 2018 17:34:43 +0200
Subject: [PATCH] repair sessions
---
examples/stdlib/array/why3session.xml | 7 +++++-
examples/stdlib/array/why3shapes.gz | Bin 3611 -> 3637 bytes
.../strassen/why3session.xml | 23 +++++++++---------
3 files changed, 17 insertions(+), 13 deletions(-)
diff --git a/examples/stdlib/array/why3session.xml b/examples/stdlib/array/why3session.xml
index ea77f929a..ffe2f5068 100644
--- a/examples/stdlib/array/why3session.xml
+++ b/examples/stdlib/array/why3session.xml
@@ -110,7 +110,12 @@
<proof prover="3"><result status="valid" time="0.85" steps="815"/></proof>
</goal>
<goal name="VC exchange_inversion.2.4" expl="assertion" proved="true">
- <proof prover="6"><result status="valid" time="0.92"/></proof>
+ <transf name="remove" proved="true" arg1="real,tuple0,unit,map,zero,one,( * ),sum,get,set,([<-]),([<-]'),make,inversions_for,inversions,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,numof_def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_some,numof_change_equiv,sum_def,sum_left,sum_ext,sum_le,sum_zero,sum_nonneg,sum_decomp,shift_left,exchange_set,array'invariant,([<-])_spec,make_spec">
+ <goal name="VC exchange_inversion.2.4.0" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="115"/></proof>
+ <proof prover="6" timelimit="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC exchange_inversion.2.5" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
diff --git a/examples/stdlib/array/why3shapes.gz b/examples/stdlib/array/why3shapes.gz
index 2c609936ca4422ce5e5914d2cd54336f4b15994d..cc5d1393e4228bacb65f934aa31d8f75f03bb9c5 100644
GIT binary patch
literal 3637
zcmb2|=3oGW|8HaO=HIpus{bB8@%vGxIS<V*=xwu@)5y^M_VhvhcISiV^BPRvs=d5-
zufBdtlJ^pq$W4z;JYO%rVRCY&VtSpibD;1;m8P<;K>rzrXS|<nb$h(0&&9QP<Im%+
ze`=}|^YYLBKXcW0&#&K)&PKbNJ(<5+qW6o2#K)fMRUIlpi%V8aG57E>zt%31_io)k
zE_u7Q->ZL@@6I$!Sa<mB@!$4lPh#y%&wRg8_w#A)wa2ygrzS?VpT7TD?)6mOwi7Ch
zfs-^|^SZuUyj)OO^nhs3&;8zi@}F1iUij?t)%$0U*YE%N(|-1mD{R_5mnVHZt$O(W
ztb*G5=~XIK{PMTw@7{R#&fJXGKUH5}`&-!ECbM|)9f71|7ttl`4<=bi?Y-!>^X{Uf
zt6#tFyFYhH@0=QE{oR^Bzg_k}`bzbe^uD_C``?8{7k*kOeUV$qh&4+^{PkU%{Uu8O
zwj}c13;i)!dg|xpYCnTt|0;;(Sp9qD7e5wD#in<z7nlXV{MzKj<8e;s%OywObJOw_
zgnO7p<}jxSAC`H~FjMJZLv@3eXM(iG6vm3y`U49YYKqJPy%aXBv}R>8Q*~PAWN=0C
z#Z--t2e>Z#db?K}-@ldj>ayf}=k|$Tm+9>eJ$rU~*tJ~`8~#n($ZfGuU{gduB#-9w
zK);ubTH%4IpI1iO2D}fK%5CD{_3J#aWm}7KsZk}z<E@Kky%Bh%7jvBd+pksaSA^6*
z<=>XGPd`$@-(lI8(6{5|ZAObpZPP58`VUQ%{1<v||Ewqfw^&^6h<L!GcVwnyqL4tM
zXh#84#|O@a6$?yTRAN{>7j2v=8JMcLYRv@s1TjC!Xy?4nt&KOdbDh_1+>`SpAZF^}
z=@N&;&j%E?$1ggte%Wz}11_Qmey}ur<U0^HV}s(tM&Tn7Y=RmSPb~;Jb?OAub@6B3
zJN|z8`tR`F@Y~1iat`bNW_?;)GATIW@2!ix=gk_PF6d~Ue<`hP|6TcK&yp)RHk*~~
z6*?7=S<=Hh+08md(@!j<O6tIJfegcDNzJH|#AaQuGyKbPBs~Lnx}D-oHsMHX>WJ~+
z_1fhTE4=uf+sxOmeWm03S`}jow3=O4o3byq>^`yL!$Ae^OE>r?{LkL^<glw?NuJl%
zhn7LPQ`Iid{Puj}u@bJs#;pg}ZH$=EV<g{t%DMDu>I$1{p>-ZB{zNBEj!4`p)9|!`
z_2=oQZ>D@MUc$nbIU&RKQXv1tsFyQBH0Lw2Ui*Ec^49P3^6S>WdzYSm#xVPeYAWlM
zugqm9ZoDb}wv%J_r*Aq{g%{LCb*<vgUC0&gU%`^ZqHpQ@;vkRntCe9dCcinUSE%rY
z{qs}r9Ute)<*fXlvTeWp4EJwqCo2Efy?pOf#J2RDrrA!nzDII}rU-6f6Ha9~z;19b
zTlxV1{f0S<Pd8gg?Y#8$l&aS;mP5g2XBV0H1UWJvoDweVaB$Pwo!s?i4BvN!PAulW
z6DelH`mFch3Bwg4Us={3*u8KM|79M5lV7?wh92!XtXMO3Zsx_xh3l>sq`hg$%0A_{
zEH+e5>sQK_{zIIn_FRe+zA)ue0>fqbMWTh`^)qj47Z=w*Y~Ibw`OAMXXaAE~*6mST
z=Ox9vycIhgmaV)xZ<of_{XdGN?>v{DFEsDGx$))82fut-GN($vWod@a)B`03vu0>W
z@^{wDFAflox4VCrKl1OguIiS6z|~tmO`Is=&9z9?@T4WnqMc?U21lnX4ZN2k_S5hv
zAM;ACubPJ&Proc&BXRsxq5JO^@#jL%Y@IHt=1*+iAkdKQc`)l0lX}aMC3z{Gtn>NG
z`-Bu(Z--c~jr^r-6J_8jFuSL1_LNNq#);=XZ*g1jyTqvD!OV?pA-@EqWSrD?G$yP_
z;@LUZ;7j`UcK6lt29t%BPI<tf+~nfkv8m5Huk_TL4(*K#r0+~zRZ-`D%bm@I^^pc^
z(m{5;PXCDaOO!Ofm}#2a_1$xNkzLH)Kcac>jd%@XPsdiDx>>7OxhJwDQ#|v__jj+C
zzkMF>Y_=))#$Vr#(@`2X&VE-kyl%2~w!<>l$B)EUn3V2r;hQEX`u64Zgn3uC=&8Lf
zu(h_oy|w4l?<C(7kFU9yFArr<cDx<Dkay);@3k*KlrrY<H8u8XnD@R;I(Fve-TkZA
zI@X8P-BD7=GuZi9P(L^MmPTACe_Xb8jiSL>Wit);BeRc{TBfd7+Y{cF8ghm0YuhBj
zsmluQaxqI^V3!JMI>cgMVv%|KhR?2`HI}&_dm0s04APc7*UZ^^tV^KQK>XP|y*qgy
z%dC%w9o&^FGw;!p{iPE^7G*xYvgyUYW&L}t?iM|D=8IXs<bqFSzJbRwC9n0oS*K^W
zSGT=dQT43;{El|T@B01*j14XupMCMMSmY2LaHTSf!Rd3uq8n2eZq40TxaH;9%iDi{
zzuPc-{d~LQ3y-zr7*;U%*89B-Tb}%8;o_gy-(KHvt|mW|@AH#w4(9#=r89mwOuFJZ
zsr<BSuA%PC!!{pfwan7)d)`^b_1R_C^3anl;sS!P&*P5SoQ_fma_SZ{eZErhrB%53
z#**gGE!zurHW<9#xK(^}R;o8kUW1Y1J*Hi&Ue9@(=vY2a##ee0(=k@9%S~^cpRYP5
z_Ih{BgHQ&pD;`Ux7^bIsg{<(-G>n=ZbW$WZ%;C|=oPGQ?%bgD_cW!v9_QS*4KEPcr
z`D6d)gOere`yc##yy{@#`Cp%={tOopVdZ?V=+lX%98wlVOo2rk99QM1S*e)Med+Vi
zbMEuYv(Ir{n|~+LuK%TvtJ3|+F9jO8Vjq~e-qQSZO-PjC`NiVtI>%4vzbfSmStZ;$
zqt&g}zgpYStLp$$|3S?wF+z)0JiWGb$*Bc@r&U+)VYTPtcCY@j_l@onmYG$4Td(vL
zI4%C@=BZ^W7-n&Bf9{qYM;_Z;TVCtGyWOaQW725`yG4c?meZq}`j{LRTfV>Nea}{k
zQAe4lbxMzW)?{{HjqD4_T`s(pYB9CfF3)_QS-+UCDeJN80;5YFd$!(lZVGpr+W+nL
zQepkt`rB{c=GA?xw!I^%QO4HxyZ(UNH>-_%^SAFcc=c;}TClp`;p5qVxA_as-q&Hi
z)_E=0Q}0VZvYwn+Q#MEQe9Q+WuID{l4+_qIwAtYIoxGQYANm*fJwN>5b7H~Vcdu=E
z;w+z<E<R$cyK}o6+v&g!4$aegjKZuL?Ks5mU3q8x<c!%5TidTM3Udoz)|PC1a&>3z
zN#0{GI9&Bgx?Zj*K6O;1C9%(t{d_6I|05eK&mNUup!WH~jeVKyNsK0!))j9T;#HG>
zlo^%ayJ367tT$HWrvn2{i>YiCcjOn*llvg^E##2gq88VeOBM>`d@$5_75OD5Xns&!
z*yiOwr5&GclKJ#!_tuT99se#AE*F}-Z&UR3$V2>L=Khg+)n&W-Lz}7vs%q9}yyD%)
zd6@0SbA|;)rkoq{RQabr{BYH>@xaQoTY__IHoE$+<qTVykx|m5xR^WX>t?lirXNKf
zc1&wK@r?E8iJk7J=U(;Ue9H7H!Nn#!$ya#3g)Ga7knbnwSBqUavGJPm{Mg*}$$BT&
zE!e;N=39<Tr4>)TFFk9~^pAGvEuXtvRdYqEchi!d3ll^xa{TmD-XgmBPBrT+^ZtTn
z)pLQXE=*kJ#<g{#Z1FY|;gY{6J`|OeEH5vSDJed(aO+1$LBUEDmf2PTCO3uJer<I3
zKHdBNBL9^1iivjTC4PC%^O&f<<)y%(<658Q@X8kb*!H=ZyGG*6ddVx-82X}`=cdOv
z%rBpt{_Vkp&BxygzGC{c>-C+<_hp)*cL!f)-8ZppZu+z;{#`n(zdjzgcw4x0*O@&V
z=Q!F<`5nODuK!_4!VRypxf?Q^dU#eCMZG@Ix!p)=`Fwo|yMp$9lNb3rccxGOmN7kT
zX<%E`(Vk$>{N7JCT8>TZ@=HsfSYG{lv7$yuG)^RDZs-q5eaDK%jy`LqpiDu7McW#y
z(q@16eLU%LyS&u_tJPn-L$Z%gSh(q!>CM(-Q>@sN8={`dcy@l-v|GaZt(D17i|AvP
zUoDo)>Dzpb_?f`LD&DLxNul?aWn$0Pi3MjZHg)b2?Y{RQuQ%1h)O2k$vzWD;_`Xa3
z3!H4~wD)Dk<e%2pnVngF&UVhq%$zi@3r4H5!ga4-6}_q5eJsUPMS5MExvO9ITJ_@X
ziyrZ>F0EaDXYGyGdD^phW~!NQwev35j-R`mb+v$r$14$LHI{B43Ae4KAzCjh*Y=&Q
zV@)<?J-ntOBJ#in-MOEl&C~jY_J`=oNUEOns=U@!E2eegduD>`e&es}rYO{<-fE8#
zdb_gEOpWEc%d(cXkIPE>*q%(2TUWbhS?wZ?S6!Ajb}qUSAhcjvSN~TT-nMzyinn|X
z_j_!)LDTSS*V*@PSmbisZmBF*o>VQbc~wtxzK`T|b3LY|605gzexJQ?&CG?Tvh9{n
zaS^R~(J1*X{zJy>IlKpc1yy+S7T=q5<j~Brn<omEE!#L#bK$kj37ONYc{I27x*xpk
zQ@eusLFTd>mtVIpzqoi(TR_-x*{d;DOTI00R-Qh2+4)z0A8+Wef0g_o)0NfOuV9J;
z&&L(By8SqKEO|W^&0i&Y<MXxqyX61c&UKgh<EHJ~$~EW6lj0>-w_KhdaL9ks_}Vo2
z3-7;q$8Jc+)HA(_Yv5r|`tEabJM)I>W#?{lZroj4oa*du=y$t9q%3&n!YpU^9T&~y
zTJGvxY~z)_b>mbqf1~hXjiyOVu_9ia-T}prls72N*-^i6M{S+|@=LW3Cu=$^Yzcc|
zvi+E0`#cTR%nP^JlE2<7_>{T2+ArLu_Ry($mqq<wyV}ODa1BxFy=5;pYXiq#^OI7E
zMVD^;vD1}Qi+pl5vh`wS|6<qIiy5Bl@`qWRvt%+oGdZGn!8z7O_h*5j7v)#Kde6<;
pQP|<LY1f{g|LbO1b>6I&u&Tdc%+h(iRAJXI`_642jq^$w7yx1N2f+XU
literal 3611
zcmb2|=3oGW|8HZx^QA3?_Pq}OVJFcLTEl!Yq3I}>fx(Ozv0XZ1jPoU#`zCLkd-G=f
z{x{pM_?B(HsvFt&)<xZ0<Yd)`SF5$mW{deLWh|HY+9G*)PfA?2$+_1aAtvIp>tl|b
z-!A^_+qFOEW9}YVy<h*{p3)TOe>=M_dh|C5p5L*&%R|Z3tKF-z`AA7}ZO6lB?_RC{
z@GyDD{$2IkXQwegv$|8W=YO*Ey{Ey4Yx>_#kH42@d++;VnU$qG{@A|X7<V(F!$(L!
zwR6+GfG2iUQief{F$ZV--+knNS>JZ)EW6mhcWeH9pFRKoW>25o4TmgrCHKb|{aMR-
z{d@UJ_eI}7Z2Y@Z`u5qoo!jPxM=t+<T$9(*&3&ihkz*ZN9{dMX3r(sP_ZC?%J-Yh!
z>%RMQm-No5an|3h`SaUl|JH9pe|h8g?|%Qgvn$}|h29sef-@OSCv|_#n-^~-Sbxia
z{k_(olf9>Y22cL8vb1)GUdz?LAyw*4a|9f}E4^sssH%-rWm8EPt9rRWE&a6l1kPiO
zT;~`!btd+eH=LP}aKP4Ks>%jlkz)*d4%t5lV6d~Ct)VJ#^U7RC#@RxO#)=ZR1irXU
zsYqyjt#<X|y|df*&Hhz#?)QbnCwo_(_FKL4_oc3N(tI!SC3iOnvng`7o=Wmq>1LVA
zzUs=NQ_q4omo2!r-sBdGpwt|p#>`w!_g5)h0>`plO>Zh5iQUmB|K@8b|4LQAC-=A6
z)}8D4C?`-Xb5N%6@^<C|6<*y!7Wr0X<3FqC)SI6CpINv}aN_~Vm=0s(Ln;b~v;-cq
z2s{*K2z1Qm@Z7;M$>p)J@uE{sA(4vq2Xy8XZEL$Dl+U~|{8n4c<I0;S7Vgk$*Eej@
zpSSQ4-+q_Ic;9}*hEA=9kDLsTWgFHSBsx1Wt9NYVQ3_C+>bP>s)QPO?^v_H$`2F(r
z-}c?>x1FuM(H8%W>uGJ-q~L_T?_RW}a~~)QIC9WG)9~>9cl^bl4Q-Z0O7Du}OkH7O
zb*#;EvFxTP>fBnkybpr8w#+!#Bci)&!$Bd{XY9e-dX}t-QGVKDD8*vz=%TlTO*MAO
zx|4zBi_d)hy6mj}@k0W77E=!{x;m@*;vCnMkRJ&XSTl3jPy9EH|MYN?hn4x#n;&FW
zZgZP_)93f+6G>Lh4`&`sxE`UQviOYq%1;+!Drai-=T4QMr1d}She}w4E_;Gyg5%#J
zOY5h9WL7pfN~uIm%(>#cB+N=JbXB@T<5#<~iQoQxZhyUc_wSpM#b=~SJwq8w|2D`P
znZ2G<t9NPH9^2D#GGAO>yZfdam)t(2tko!S(A!VA%HZ&Xs#T)DRH{FD%W(WYSo2dT
zuO^*6`j!36x9|DiO{~p+a-#n9n(ao@-b&7Xux!G&+At^4P?og^U1l<TVD$NLi|NB*
zafRnEJ}LCMEiBnv)H%tp@k5C3W)0rSAr~ABu3lvc*pQR??$CVR1AFs=pWI<8pT_Fn
zSea~4#G{pJ>!|%9PviYz6J{5qy++%X%_y{JS-;6x*GhlOR;hD6%>lm4-=tg%eY!Bo
z-|e@?oCRmJ-<mS|YVxxg{8fw+EdMxt=UyZ8@8WhlZckY7-(=bck99kXS1kQ7r*Pp8
zkx3jWv!dRv><;?ft-t+X?Y@sIAN;H_Hnx@Z@%KNq^1D++*Rdc@ANIwaos&LJ`0?G4
ztMud3&v*Y$xSF4}!<|EPtJkdlo+U9s0=k`^2Nea*Ze7@*xm;)NC$-Nf`ZdcXJVIyq
z&*Y2o>rXyv5!PpIrM73s1Os`&NxGHYGA*qPG2UEZ!QvK*Dr&{b-Zno<b`($H(7d_q
zR_57D@((XIc{bg6VsdB6q}G|7<@1)CGTmK1*^%XZkLiL-?H3*h7#-wgaTZNJ@wR2L
z{cd}kTYnm6hG;BhVwVt9v2vPH8dJ17IMqF-llAU{z7W+<)|c#z6to1~H3his3Os8L
zRjG@5uH5dq@@3wmSkbQ!Up-r2P(3}e<7L#lTe0Wfai9Erc9Hk$B^U4SUO#`^{CeJ-
zC$=SiH&@ilUYKBhzx_ze<t=$aGsSwl;}=}IvR23{!YyRW?)c`)pv${vtU3HO=YP(1
zqgC&@=T12O(#3ptD1)-&?bwC9D_<_XR<a|GVRmmqg7PWf$Gc`2a#wwSpJnyp`>Fn5
zrbleS7IGginJsI56#DtW)@_GH8#CoLI$A2-Gg)_9v)cIKUPGP5i_BJ-Pw81<()&70
z;zonrg@r;QYCjep_Pl*8?b6hwvw7X=JUohxhRU}7nX661T3$5oG$=2BSk}G$w&gaq
zYby(PbWi?&%`vER+0@w6i+<0x`~E8D^i+P!g1wWRjGyj3s4%ljW3Sl?-F&%slB*WK
zn)%=Mv0U4o{Wb?#7=(__x@-KfgDKZB@cBwcj<d{NNuh1`wjDioagn+I{df1vne+D5
z{gP=H6E;fyz$W#7&Zf2Jj@@u}|GfV8`oy_M?_H98b~3jyZ{C7e1|J($R!&xVKdt*#
zQdCiU<s<8moICp_@6Z)})@kCudJ?z3g3_*YdwVLUZgp7FBBq;lF4*}}={mh6Nw(*l
z`45X26R#y_>!)2kJ&ofIL#opr){@ZcmeGfs-q~2r5>rv_;r3a^db|BxXt(Z{-7ybB
z8Mv-^ESX}Mo~jkH!aLP4YPQ$ODZyb5k51O?^RHPRd|<hA!&AK<9`^PZ+~gjA?Eidl
zvSoe$gP)IA9V|Ql>(kVu;UXfeoDUX#I<b^P%A$xVuxNwhs{ChGD&=!udOh@PetvoP
zIgV@dZ6fUYU;Csg-Jkqgpph%~fl2Bu&Cl0_L>Zo6ES_$2{B*ulDWAzI;iWTLU2FZb
zwGF+x4lwl})VvZSv}ncCYfBfMTJU#TcJ&^1doFJG>@R!Q=q_QJS>?C&N?(D~;*V~g
zTBd?w76<p|Zrh>q$i{40t^aCw<%ZOjg%c)y^vFH*;K_0}+hsAwCZvBllfL%-{^ehL
ztvFWoiZ`C}Q2uzWivOe|XQ<t+{OJ?+efgR@eY>^wjrCs(QWr!>O04_O$bIwnk#9$?
zeLJ!6_59sFZzFl+FMK&|=bH0N<N6lft!h(NFLA7Xa$-%{9L@7FAC$PB_iQ~VIA5t|
zM(wA~CC(p@8y^2$_NdZ&qu=+hdFt!te3}*bXy&v#(aOzFH6j)`db>%keyb?g!kwSx
zf224~`p>+1RbLLQw=lD{n)Tt;p?y!-l1o~Y#I2r|T(NwbByz~$_>AV~w+_`ly0b^@
z5x>FY%8Z=*SD7|4NM&B%dD*4;WV_2Ou?XQex(n2HpPOsNl{M2TsCwcT2f;^-=QI6P
z-zs`VO!1TAI>;v9yl9^5dDX8OJga|R{xfq@kZ!w;V{UB@<0AW#J2Q`@ta<ar%KOK`
z*UvOh=bk_JZKGEKzf-^eGM~N7rVnp0{AOYZ;oHt|ZSRwZ7NYxhDF|3x^|4+Qth4RK
zO4EZ{qP)F+1}P<u>*}^0*{nKGN%rC;ft!0CiCKQn*tvO@=E4{U*`AJc?=_K+gr_$%
z%zSD0bModUDa&is&sMK~+qjSQs_2*H|96Qh`m$|}QO)(8@oEd}m5S>-gFPK}gE=P|
zIXefXC_k}2dm-#h(R<O1dp0aQ(=6OqI=Rn^He1pAX2#y7Gnc$}Z<}7cz`Az9;{~&I
z`PTOGcXgalR=jaX#bvU7;)?w0EnDvVQ2BPCqRoBd=dOkGpLFt69-76cShGg){Lc%D
zv-5Xb>`-WPtPj|`jM>7AefNnS4R-IX&aXMBSlxeH_X_Ki((60b_gk`TFWbG0J4yMi
z)%g`w{JV5me|<b~@#k-s*tClg=N8DFs$J23INTw~C}-(2vj`JKH?|PTwWSY^L`(Kw
zK0lpDe#aqqt1sJQ?i71emw0Txq~W|b>DbDY?QWHFQxy(2_g}L5H0Rl`3>&*nPJOR+
z=hXi6v@7g!a5*l^xN-}JMBr@)+s$XCy9-Z#JIp^fVeZ*quCul#p9qM2JnNNHvew*Y
zLx;6ReM_9GZbtUZEtQR`nPdAnrfQCNzj$2Lni_+arfx?8&k1gC=NKHj<*_48=H`*J
z?A`Ym^X8^{n3}GQW*4(|6W=HDZ-cW<-TGabG5PTi;>|AS&9AlyzI@}%lm)3J`cYpG
zEq^y_+oxL---sP*Tm8^;;^m~*Cl9S%apdr;vm1gRhP~n4F6!NOX4352N~a67<70QQ
zt`;!ycqPKD#?tL0;kLCjMC)bcTeT^F*^XtgwcY$0{8Y5!?NjOfrODqUK6-CGG%<M6
z8>17qN+-5*eySCV*!cd;9_{Hj_8Gl)*6aKh;w~-RRIL>3c(|hYXBXR(X>xhBd(vtb
z?GO_w-cWor)zq_LmZqIqk%>grtrHjTJt&-YqVcS%>-rmi&pAH0n76{W$VzGF_lZGo
zCw)E{Qds#|DWGd()$Y4>=2J|~Lw>G3xKbsMRle#$+h1{;Tk7e;8~zz>UD{{)-Y@B)
z&+e=gNGJrnHaW3nwQbv!TgMhZ$b8nekoiI8vt0|W^ZPG$SLI#!My(*E`00dO(R{s5
zezWX$8_Km`Kd{)2ZC+T2!DAM8&LaZ-t1Mr%9GGyqLFL!V+s~@*{R;lRc>nV5j^_Ir
zOII2+PTo<|7vjGAg^a|DUYme;W54?k-e=C)d+@9Jfp@GY3KYuD$4Heil%2mLQs(p~
z?|#h93xR!?&E#6|hUBfdbwMz1OD}t(x%ZaD!)<okKHYJCa73eP!4e1Y)}TW|SLXcS
zSmUAoE?y&V{{71<OX7c|a0O^A6tz0Lw(!hCbuUk;E!z%8>@}ZTbL+R_^7m(I4($d}
zYvQ?oI@vColzHW!>Dd<d7kgc=aZH|k^x5;wlN(Mbtv{#T<CiU?8zs+bkzcvtP~kbj
z6^ZkXWU-a*3o3ge7b^UB<GbG4g$#y%6Fti|XaBq3ysRwgTVC6_{4YF?k4kep*8St(
M);%p`Loovb0O8;W{Qv*}
diff --git a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
index 7cc3ebf48..7244f3069 100644
--- a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
+++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
@@ -4,8 +4,7 @@
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../strassen.mlw" proved="true">
<theory name="MatrixMultiplication" proved="true">
<goal name="VC blit" expl="VC for blit" proved="true">
@@ -216,10 +215,10 @@
<proof prover="1"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC padding.5" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="1.64"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="4.95"/></proof>
</goal>
<goal name="VC padding.6" expl="assertion" proved="true">
- <proof prover="2" timelimit="20"><result status="valid" time="1.67"/></proof>
+ <proof prover="0" timelimit="20"><result status="valid" time="1.67"/></proof>
</goal>
<goal name="VC padding.7" expl="assertion" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.78" steps="919"/></proof>
@@ -262,10 +261,10 @@
<proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC strassen.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="VC strassen.7" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="VC strassen.8" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
@@ -775,10 +774,10 @@
<proof prover="1"><result status="valid" time="0.08" steps="142"/></proof>
</goal>
<goal name="VC strassen.145" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.44"/></proof>
+ <proof prover="2"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC strassen.146" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.43"/></proof>
+ <proof prover="2"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC strassen.147" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.16" steps="245"/></proof>
@@ -915,7 +914,7 @@
<proof prover="1"><result status="valid" time="0.09" steps="167"/></proof>
</goal>
<goal name="VC strassen.163" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.17"/></proof>
+ <proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC strassen.164" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.17" steps="294"/></proof>
@@ -961,7 +960,7 @@
<proof prover="1"><result status="valid" time="0.07" steps="173"/></proof>
</goal>
<goal name="VC strassen.168" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.13"/></proof>
+ <proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC strassen.169" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="308"/></proof>
@@ -1030,7 +1029,7 @@
<proof prover="1"><result status="valid" time="0.09" steps="187"/></proof>
</goal>
<goal name="VC strassen.179" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.14"/></proof>
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC strassen.180" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.35" steps="979"/></proof>
@@ -1075,7 +1074,7 @@
<proof prover="1"><result status="valid" time="0.10" steps="196"/></proof>
</goal>
<goal name="VC strassen.186" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.14"/></proof>
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC strassen.187" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.38" steps="1048"/></proof>
--
GitLab