From b34edac4013ecc0392fd33efa6631e4ff0cd1701 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Aug 2026 11:47:31 +0200 Subject: [PATCH 1/5] adding VerifyThis 26 Challenge 1 --- .../heap/verifyThis26_01_hIndex/README.txt | 14 ++ .../heap/verifyThis26_01_hIndex/challenge.pdf | Bin 0 -> 47216 bytes .../heap/verifyThis26_01_hIndex/compute.key | 89 +++++++ .../verifyThis26_01_hIndex/compute_opt.key | 89 +++++++ .../heap/verifyThis26_01_hIndex/hIndex.key | 80 +++++++ .../heap/verifyThis26_01_hIndex/lemma1.key | 86 +++++++ .../verifyThis26_01_hIndex/src/HIndex.java | 224 ++++++++++++++++++ 7 files changed, 582 insertions(+) create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/README.txt create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/compute.key create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/hIndex.key create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/lemma1.key create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt new file mode 100644 index 00000000000..ab45d06cac0 --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt @@ -0,0 +1,14 @@ +example.name = H-Index Computation +example.file = hIndex.key +example.additionalFile.1 = src/HIndex.java +example.path = Benchmarks/VerifyThis2026 + +This is a KeY solution to challenge 1 of VerifyThis 2026. + +The h-Index is an (in)famous metrics in research. + +This challenge deals with efficient computation and updating. + +See also challenge.pdf in the example directory. + +@author Mattias Ulbrich diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf b/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf new file mode 100644 index 0000000000000000000000000000000000000000..d4a8a81c29fd4335826962d9ccebbd4f802f2090 GIT binary patch literal 47216 zcmd431z1$w*C-CsLrIAsF$mHy%nV)9-Q7|{cY}b^-Jz6#0)ikV4I&_*APp)K5|V&F8>Kc-|+Oj}NQ&&+|2e?W}>PRa9R~dvC!pcj=+s(-y zm=mGsY+;K4=0wflf$;Q{b9M3Z6!Y@%2B!6Z^6>!ZsC#?4d3(v(J0ZlbgRg^xz&v1A zO9zmsC`1L}V(VoGhVlSSS`Yxj3*iBV$T=tr6nlAWtt3goQK6FZZd5V$wAs zlJ+|nDbG4Y3J*tg7K0YB8L^?E7FpOtoLbtB@Oo9j;_)SRrxw;xxCo95iHm$X3<)nR;AwEotqBh9b0`eJv;n9_vGtg?siii=39ru zmA&w&xq`k8MZ4A~1L~1EvpLgg*SF98s(ose`c8Wm(pAT94xgTp$(gj>p_yXyE$MG2QR46Idvbj9i5{lLC@R)d7Gj^ z48CKWZ(SH#y#CIo?HfdKArbyDxjm)}qN8QLCaPLgAzt@9wwMWrACk%)rVQm54>t5u zyir_TR0xG~?>X&K#a!|UWji>Gc`#$y%qPB^+_K1#6$--#YtLkej1pZR?+(sEh}G zrEta7mkv|;@}mQgN{FS0ZC!S{M(M#ZJ?;AwD`wVZtYo_vr$em7{N3^*P^)o&lUN-7 z^X#2@9Cs`wK3CCHilqdCu?sne(-@)#4`dkKJ`+xzRc=as+jS=AVazhI2+hQ{BOxR^ z%exDf?;VTH^SPjt`{GL&be^W0vSDSs=z~^i(_leFzmj>}6504bFQKwn?T|y|!5qoP zQG2^#eJ0MAwe^t#zV~v%!2yW`5(q2ObX9V;bQRT^tdlfNYy#eXYBC)Xm5GY#2>r5h z{)h*;Sqji7D%o@wqOlb|=V0Z?2d?)b9#5Ee*4C{G(0$O+n>=l-{~{cBp;A^RA={0W zR-cI_1xxYfMlp9u&-1-hZ?~b{lM*zJb3)S2r<(p}5~r%4b{Ix4yk9DR$*`W?PHCMQ zRgts49OKC@~e)SzCNU z?laS|BOZ#wL3Y;hXL!>W49Y3nufA3P}%s0I+V@hm0HigS8}(y! z3g#uFdk;TOL-0Di$SuRitan0nxcmCeo3DqsG{xpW6FQ>(hWo5FKp1@sG@LLSgumMX zQ6n#98ebFZkn*c(6?3n)A$rfzP_FF83 z;vB~V1x7PFp_`IEuL97XcMQj-rW-ea6+>mQtjCj!I20oY20L>lM0NUDxr~zwdzd=q z_^e-|3xG$m?xv>4&(va3Wm?#|V^X2bRoFMB0JmcFj;Xb)L`o+3BqnPb@q?vdx5Lb6 zBqPxoy4+e)Q4q=eeifPVDJ2H+!Pj1=j{##SNmSco_fMxWh~1Y}l5=?%N`SFA)T(O1 z2&>2|`tp6AH|n{^clucM8j?pRXJxSKTkG)8{Ase{LPGYc9r9UE5Z)(iYhw88sWici zEmRmxZoE7eXm^Lyhrkjzsu*{g2?U3fm#(m2K74dp@HNdf-wyg05&140?aeIrLgM$u zNw?5&@?XE%d?=6J?{D@fS|P8iA!@$=>9_}Wu{)_1`z1_JGbQ0?Q;7+$B3N^OCAXhH zNe&4mcQ|X~B*AB8$4en<^K7Av@8idMaRiAA?h%10E_jxjcYeO35pp55RoKXY-~`=b z(m95Ry{=G`vi6nI7n03@g2~52+CD0WccEK%8HMgJ(?#RQ?@IJ{=aDQ_lBRd(D~YFK zg@`DnB_>VP^^=;hjEN8@r;&EJtyN!Pib{`lu%ZW<6FX;m`LdxY zTj5te5qr-2*n9}*jj%bF_WtdDsD0jD4mqP64=%$6k{Qi;dz+jv7A|szV)rI3<;6{6 z-JgAX*&ZXrHjSLupS$ir0KN>$k-zEda`hrx4pk1OGbKLD{br{alee4IDo<3jq8B?2 zs9K(sHeaH2l)frbzvAUna8r{#09{1{nl4e4KthR4u;QcYxM+9x3{*xLLBwR6dbt2s zubXibw3@J7SfqO{p)DO_G4nOj0v}WC?Fz?OAT7>rgT-i&Nj|n>8+L@bR>)q=<%6)S zI_N4(N4v&r*5<1wra2rfPVsIe`>RZnT{&P=VjZz+X?|CwgZZ-P39@#g%iFpiL&yTQ z1HRyT37!UgkpNYU#kD`Uu@)z+i4JPN+GMN^N`|{q7vm~QVq963SCphlRaS)ydwt$s z4*xRWD030V*?1@y+XeUSnr6;&e9TqRQ4XFmIFm(YAh-5l;Cy5~$3-q&X_n;)TJBwU zJXvo8&R7LOV~n%VEs~xVvGCl7MDh-=eLJc{*%-?nl=7i(gxg>iw#_^5_FKIDTY*lzt zv)7`NR#gEH{TSMY1##li66;$H>@y}>pO+Smf>Jk?eANhT#gkcFR%gvQZis#}j@E0r zEJ`o@IGoInn&}gDn{*>S_xW>;`1dT7IH~%{@5dzPoFnh<($ov(6r_0h_=E)1<2vlK zrPxWAQ5A5qh^)uE_;{rg#JRyR6YolDnysYexg+ z1FH`QYxLe+rDd)py!N^-d6q5D+9HBlka&283UqHcpl<`n9^h+f#3uLnBDeY}h!`&e&{~9=` z__Q#AiB*f^6J>qSk{X2r#r7*o(*6{p{bc?O1>@hQG)#=T@;~adKcjdKL1Lrb6SU3=HImr^(E7L-^H8ttTn&7w$Ra z+@(dwo?6n>UznWNprd`L4{i(2^+k&v@#4N#Ev)lqGVc~?Kx-)}+odtCqhxVt=%f3~ zTI|PH6Kq!%RioaG@~KDAwvfxa2{P5oB}i)cBtCo-aP7s;47+%OOTaPxZh@V&M@tm0 zHx%*6Yi{5s3%_V9!=pD(&|^Alp2~Q}zftgezp}ZdMSM+51@AF>qGkE*A&Q;M?kj_y ztk*?Go01^Xx9bxX=wSUc^ziu+la0j!H<30pw40d&L7+ElyZ?6<#rbgl)>u8r|MV>sbfZR=8BUvYH3xIHRGkGVB zI*wimkfU7a2Cs_JDkQwtbCa^TqW!6*A(G5s%DLW|Wqm=$$fG|}qz)&q>&#w{(CuxX z-$0e)Ygu+J>C%GrcX^o%%D3)etQig8z2WFA%DlrRAQS=_(Bk||j+0b~HB>$u-|wnT z??0hnJE=b;1+Ipir#I!REM$F48&*<**bE+lA3v34>FuvYGv0 zSS1;E;G?{0sqI`%qO>J~0Xk6|RV!7l8Lh>|t#3iSnhf0lQC zlM)U|P>}8uVfBwmYZk*5<^^;FiwZuSVLah?nd#pe&9yM!$9n=V6c2t-|E?`5rTXku z3>K*$SMK%7NFkfh6d$`A-4n(@ls8@YWc#uAYsE@? z*tY$0!W3qiO%vs#w2yqJl6e-`DwWwJehoVyS_kq1s&LpRLrqfV!XA?HZ!5RISvw|* zl`1zaT++5E=<*Y$-oUEu7J2K%GF~)bxHPcgfGJh0Swu(#MZjpp6iB89xvrOB72lYy3uoF8($I=k zzDjO?;ROPp1lnZovm5(LwVk)x=t^d4rTjgdcW$&i%<~p~ddp7s1g_+0@g90o-hpg& zMjrV7^sOf7gr@d4Z+&5&p^APOnNOSBk^W+nfUVlAvH_nV@BuB{OHJ{-s8=k7c7M~X zsqX{xC~e0QNO^^&g4VC5^0rB~M^k#c6ZQ)WkCI^eb*n(u+hJ7D`Is7&=1K3VZo@uO zQSCeALp9;qgL0KBoi9x#uTXSxyQM5R@y!ye<-|?$S9ia}?ix4E&eD(iGPP@#8?~#7 zGa3sE&Ji|lMGqV>dJr_4ZMo2N_oU_H1uBzuE8RQ7ZaANO%FtNee!9vSexG@jp?xDr z?DV->#q0FlLQA7%O$z=m?T#(S7g*UJ!ebj*FNA5fZ*qi38P-H_Xk5=)jq?<1=p{8( zXRp=9c>L}ST6PxMQe`|5R-;W?E3E6jz@4gA4rzsczgQ#8JeyHwou0|{Qo$EN z4V$=q<;aGBfw9p^Qm%z#Jh{e4KQbBVA~Vir_@~4N!b?(-E;Qp@hJRMP7yMVB{Y!&Z z4sDc6p0d?Hkm0*f`R}7xTH{kqY}&wLGhTPFeXy&V*h>+x>3SET?$yo^{P2>`wA<)su!Ku!DZWZ#Ab^dviQl3ySa;61=vv72#@Y=Sy&X)Q%sI~&`|57E zGZ$NBt6=$C>>$FSBJ^kU_z*-z{LL#kP)kBn=7lLiAw!?=*RII~3r0e!f`c>$#NU+3 zIkL?o%&-gWi!a4kQryvbsur$%sAHro*#-+#eH7UG&32-ZAVKL5{$?a$5>NP7uZatXND{O1>rmt72@MuV39S|%W^!q}G`Q-;qa)$5E|yYqGBQexwqx-`dwF?xK=+`zqg7#as{9~ZSj|)rrlkGs zAm2fz3=A8MD(b`epf_P)P0-`Podu^l*Olz)R`6|(uRIan+=jhXy>(Uh|k^X|TBe1lmFbp!NxX~8@*^73LuKZmXtzUa1Jnz79le63C@?OcpOB;1u* z2bo&U6}MO4u7}~m4T4E-QOXUGex<%%^YDdHBIj$>naQ__cT#ZP9n>H?Yqb(z8osD* zJm%CDt~4 z`;|fqo8u-GqUAjY``bdl?i{!7Dp}ypP{zkwnp=pn%4sue(Y^r_-P7GS zBCCKVh9y;b&Mj~;j823G8;$P?Oct)nEn_tIf0nDybRHU^iquT?aD41BXZ7;hCl|Bk z^YoP!M|tCztQUe*n;&&+IeYpbUZW`R`buhkUZyOUkAq%pao!#}3~wfB)vHEF|_pX!m~)B$wROrj&etzEMJz)b zaT})aRX#8GI=d6zdkzlcwV}KCT4FQZIFVpuf@o<(Nj@)rJPiiAE^D*9Kl~Zvc^5%@ z&xU9)E>1#hchp*DFopP4f}H`O=JU;qm5(gD4sYy^9-q>0r4}5qwn}#H)f>JV*Js(m zSUHL#xcD;6Dk<}N{WImURVms_{n%ztPdg)hBp2@}z;#?D1%UyjV*4rZzwZ61F~ z1R0M~rQnI{ee_&rZ5j?cB=m>BbS+qXj_zu{Fc`5jNZ%2W{X(4}EIMFqr)PVY82eU- zPj`)`uI`b-MYD)g|E#?@h*fzCH&@69%1~12a58pyr#bdH+c$;Pt$pJm9LgDza7Xe{5eS^0@DTCHbzACsYLSayPL)m_SpB=q?` zk+xlB9DMRCbk{HBnmwwTo4Yvr^x3!M13LcYC_@5}Z#w79Zi)!5>++fY?!{<4Vyzu4 zirN$dcXo+Go!j@XeKxQ@G{J2PxHq*ZE$rqK);3xL_37Wscouhd(=v$HP#bnbM4-%vcnrCI#Sa}oV_obBWFrlZ3!f`Ido^;)M@A44Za7PL zl_s~R3Bz+q;cFDSAGtR82Gbn1OeaVxp*o0*FD12c!!VxuLQZsq`f2Yq%^4;E5rQTq z)~=NnLQ%{>&qo^T@GkS%sml+A9Bfy6V}vv!dz2R3YH(B?@10zhc!iO^Ju>gRV8>8B z+9v!q_x_m(O*3}QO@ak4V>|{=Tt{U*kUHpjCa&p3T~&FqNTYojI6n45k8b_D9Zg8+ zVdc|DJ_-AGvmCpM;wf_9(4Q2h2DimqoQb^on0(z$xgt!4=i38;Z{j6{Irf)cb_knV z-w9#m%;f0Csf~(y=a;#hb96^;uPxN+T3f2=(vgB6hW{C4;+f2;dg-lkYRFDm)`mm( zl~pVvqC0LiJ461R{CsgP7Z>{J%P~C7L$Dw_Debgo1(+Af8Cw^yQg-||W3X^55*bY* z!=oA3IE&hIlE3lnI)s_9Vh2XGHp+5eExzgjm0xvDYID2GLnCqWt*&dwl~4}4O2)wX z;P$x4G=Cf-^YWnOLL4rMQn)VB&?1w0B+(WPp;=_uO%gep)Tg8ihG>2Ut>(pIl?Ttg zyGE0lhtJ=uj8Wg0k)=9!^BH%WjElp{Gzf@coBHPbay>2^Lo9}>8b^a|!?bX-9gkrp zT~{fM$5X1vsJkRdf1+brM)?x&#eT4z6M9b@mHZ>`G|g9V&3;Q+vm=tODz|vXOYe@c z_Jn=HZz{`i;xHw;Z_B0PTnz5Yz1g~~Tx9N)3L`R$+G1wUG88vM;FqeuX%)9!{J5em zd}~O`JI!UsXPu4Z+v9HFJ9L4C_B6(m+n!W=R85wL{TU1%kZ!zCw8b~o7q^Z+m)ED z79(~g!FPBxGcdNjkc zvWm1?VbZf(hC$sbGeVY3j#U+jnEV=gb2@ikLv)w-6-m}hPx!eI6bouTH^k**+v@j( zDw}xrpFIvCcs4Rq==0js%GfYQ`TTLhEAIYiQua%i{SmsAIBBn&r~3O^F zxisD+VEps+yS}?{#+deDkYr(>kN~*&2 z<164f=iGXqV+GE(d%4@vt3IEJ!wSi>H4v%!%)xBACeQY19j}jGv~k)~uEDm`6g7q0 z7Hhx9x43<2?8x9L<-I}@%$C!8=@I+S2nPtl@6Pu6k36hTXo+<-xD9NJYvc)A)T%;;iM-|B}K%h z4@5bg-}LK{?KPJhGcnb1_=5$zpg7o5)eDY~aqJ3F*s3Qy9yM|EffSRWV7(uLC$ zc?I6|y3pkosBqKu@k}Qg&6V^h=2f5b-fh7^79V~4vVM-cI+KzC&yJH1Lg8UrovHH= z-sjEpRP*4?V&WU)Dbv=CwH|(bP2s;;r$R#a+`{KYG1Mv4LPeNNpinf*3iRs5`W|Ec z!ucKlYNm13^f@7YzGrdejRp8$af#Lkw;e4kT@n_ycfeiCX&0WkK9?;3>O^;a8B7|uab(SD0wq3mP_K>zkXk7C!@CSZ2?L2?m)5keFt@RtViTJ>@*+H zMWKPu#N4npR5I_V(zeGb?I+%~oUCiiP{ndXe{q1%{R(=G{Zp}=H(ki{5P`dP9_w^9 z#=6WtF;+KUghJKAm~7a2{Di z3?ABcfh6fe9|ytg<>cSGnceq$|DkARW=DwxqHuh3ELeHURpHp)e*3W^`t2)17v^bc zk{x;Ep%?nD$CBZlG5VDk#7}$)tiNt&K=Yvmniu9(aCN34;$&XN8E3CN$P3$+$50N2 z@Rjwu@0RNIHtpl9_v zPsD#g+cUo>1l;3jYx_7;4QdOSz(ubn4}0oGjDwGZp3#8CDd9q#YDV%8GGT3=P#a82P>2l_4CD$wa_idD#m##?R_ZAG?SN47~B~QF-Su|k{ zi&gW2eJrW`AbP*IHk(8VU-&V3u^O1YAbaJuL*8f;nX*g=X+uhOQeVp&-RKvyxA~gv zg?d&yoS!OrE-yOZhJOhl;HQqi_N648Meck%AqOn~ON$3{s zcZ1P|XG7~Rec|QJhRpY9h6^vBl98w{C*S*eDWh19b_~A&M;MU~CD|+DJyDw~n`g>3 zCH61a_-1eaa4!scKwOx|!`FC#=l`%fTIy@7pDj3%cYkD0jZh}MuhyMpzxZ;6W&%qg zu3Cy1R;8XO^RP;^%KU*Qb-6 zNy3h-VBt-jQi+MUX`fqaa&WZxLMmU1ecihJRWMplE4<0pEcP9_#eGDt%CgGSD*TdF z@hP?|1(((QM&bp?-E?i-Waf+R-(c~2a#;q+DY8Bn9;^K5m_2Q6! zyQ)*gv2#Ohw%q-(gH3evi_cR&^4G-9WKYWwsW@+*dNC492*lc(-*L(9m55AW_G;+AI1qQ`mj5wg)&}56(3iEPA$2+`nX=!)}XOloj zzRu!y01?K$=eJjR=Ffp_c+HYJ9Zm(4g`fI{j%d~7gAK3wC%j+8KDCXn7r5^+Sb1j` zhzRR{gx0*Q$^58pm~(0N1d~{U|KX*uoXdHdqtwe`MD#XrmD%YlO!3{(P*0= zYvh+=+)G&IHVl|f{nfY@&X1lL5h%6Zj`3iWf9x5$9bEQeBXc}&S?q)Jeo^vH$76iH z4&B8^;neSP8nI=(4(?ykXIjszY5q1KS^egb>p=Q2Q@W+NjkgTh1(x!h&da?QRUF=V zTB-$T5lyE1VFzY<#MWb*O9kr4mA+D+f1>My_&kbf7_p>`_Mm~;KQ!Uva5{rY)>!$s zj2Z0RVFMHT&(cH%J+)Qz9|kfnyF45?S-@pK9Hj&=dxk}0SV>2i3bJe zpr=pwdk0O#4WuyEHmIL=zAo@?o^0YYpLuwhM~$SNJ^V%8(@};S{P`wbAHMVsu}M6C zaDR_mXhAN5<*W9_&ZaYs?v29f`BgA@YPT0+ePDb)o8Zu?OMKM%`p_xMb74Q?w!9^t z7B(j;c6)Kzh^#KBf;!{kPCWRtr<0``ABuW2qta6&NUyjwgfcEpQxse8n^3tzyslq$ zR+zpJY~GVpTBSX{nYJ+zPM^lnKn-6h(!D#wF?zs0(4oH;Tl}6LUaDU-`K^Vb**`Av zIaS8eG=^JoaOVnG^iAhF^K1BS)%~yfQs`tfx7Tqo7Am*=8qgTV{k#X-cpij>fVMQc zc2=(OI1=XGVs_~3F$>npmZjoS4SB)++0vCwHR~WI!0!U}haf1febXsZB84(VM#WV^ zB@RcHD+C`tx;!t4oZw6SR?p-mPij8Bcg?pus7X;}J4itw=k6yhob#Fm_Ws{4>g1wA#(%}RLJp7`V_cPEZ(a&E#l|V3FoJH@wQkxwus8ha< zaQVpF7y8ggc!X`;6P8s_>4keEP;+}!l6vh;JEfPRNf744&%~mSg+>$vd?e+`TPu3^ zZ`z7X-7n7iJZX}JR>ICFud$|wf7`>+Gk-~jppouN2~j3)`wi!}%Q>rXi+MY_xfE>+ zvN?wQ8DBf%PR*dvJjl_G2q(nFOg1MVf%~exn-YH!#Er&zP^s4cdI65CM8@_K%L5^D z=_I+U)Tx**U2GiA4HF|X3kp58ud;A>;A$UkzA%nCynfN^h7$oeN!!86A2%Cag@`(u z8RzAa=+jm=weE6_4Z;-f+JNZVz*Fk4#7p~0d~^|mV=jZi_fl3Mi!u_eZ$yu5cKd2$ z7d!USR>}1ai`9ooJD0wKJ6k6TwXZOamYbYtvGF7uQK%h^EAM1ol^=I z&;&JB(WcT(Ya5&M`_|r&7A800Y9^u2rpx)8P*&%Jmd9#{ped!WT~L`~yU{s!9sJgb z>58iJ31@!?xH5Q-g`=jjAO8WhFeZJ(9{1htg@QNB0u}6omF;gwIrm{ z3UR5Jq3H6XkiDUMLzHUeUc2(4u}}13M6M^2(1o!^3JN+j=njyKtw{}2YpC6igvwqQ ziLYs+EIG5_fGz%y_)Uli95b$GeZooZrqH%J-w^n zuO*aUL3U|5ukRW8?7Ecb8^t@MYHAJ4WYR7|XK%U>ZVME1uaaATn!2#?)n{MCu-ann zZ}BTCE=9(#aQ;8ClD{P-b^P5B5DnlcFGLk#ZEqpv>IXJPhO&G@eB3ZWuplp#TTsXp z1krN!0?y`wc>q`sgo_s#j!a?#%?M9dZx1VkCvc`$!^71|8{uUP0ge`fAvy>@FW^2| zKQDQ0)U9yX_gj$Xgu(Fd_XDSVA(AdGu3nzTz+}h~;ixzo1cxGPrVwcW7?{ozjEuOo zKmh!Y#47B!5d8o38op!v9X}+-zmP&@cYnu90KgJSY=9d7uaWwLu)L^*G6;e~lb8P| zp?*X2uf#(V|2vuhp8x>>qa?r+3{keX_5>S)kn*7gLXlVtgj|yr$P^5W=Z)mtZ%jZ= z{O56i6W>nuF2K3)AJ8!1P`AB@rxzH778s&p0hCdc1pmQHB(Hy?8gQ?LmxYt7?N79R z$l9;5f2YhgolSm8u{aj{Bc44cp-lf$R9scl??=uK>&;TIhlc>5m*2Q z=#L<`AXJD4?Bea@1kCGM z(Y~t@2qNX`VGSImN9iyRFs}kc5fE6gF_Ol}x)yMTA8ZWc<>BTR;s?WpV1Smxz%X7x zZa!WZn3sp28wNw_`}Z|{7XdH?xhR;R05>l$aIPOJB)|=Y@&8(ywzs7h(u%0qyEy*B z52eTdZTxtlJb>8&@Z*Pb!-c@SP(f}1UMLvg2sa!q__$fDkPx6a+=tR-gz6K~bs&6!}0_6cB$FwL) z{1{fs!V`hCiV#I*O)W`v4rx^#9ViTCC;|Dl^00UFa`gbizR!j-*hpx=k|Ir(w4H?q z7%qr1S*S7;#s|^2xAwC0GzRlQk)%cb{<-w42Kw3e*DI1y-#@?i04<=O?f-K9m;PTf ze#ZxZ`lIE~GyJUmf%nfA;EKZc?>&FCAhANiqkaJimvsUDO~>BF79fd>q>HEhuli4O zfTSn%55Ayy`d7Xf>dPpp>LK}}_;VKOFGWP#ot$ZcRXoAn$);jVQhS>l#&LG?gW_fi-Fy0*E5j?l+ADOzOXK9tQnm zjX?RQLJ9~7{DvBUDQbj&kwsMR4~$TR{3X0di}9=SSIL&Kx3NJ0-Y?+p8iRnjZGrz! z1O9If;qGnWWcr7sqio_|*DI-{W@w-WtXB~*L4R8?9A$C;Mbvr!STGa@`?X>|7#|q< z1=s@P`w!Ur2V?)C^nbknPqU%s{n_&S6(uA;@cPjXLS9ig{_9;oApgWal*ir*T87~Y1L<|TI zdrwDa3okpsVSz!cEo^NO9>4SK4+kFdYs;6BS5VSd02EH^@9GA)ZvSdupugKt81EnI zhTK{H`SU081BU1~C>T(Kqnx$>WPcYx?Ir@KO@UvK2Z&UVTObeM1|wY*pbkiy5R@N` zgahUQAz^?LU~u^O_<*Pb_PyuVp7a~O0FHd974QPa6$y>J!g&A_0<=9P zpa-=wxDeoZ3jxrAf+$En6#0-U{rwIo5DWcDD!%(u|0Wg4-v6Og06em=^7cZ2pa6pq z&ej&5cE5=O%D?@q3ad-2=;>*o#6jS%+YR)8=V=;)mk$8*$LK(;1~3a?BrqQzaQFi9P2+^6{Lux zR{e_}f1$xon*4A3;YgMO5PbYVBo2K4WegOIAV4<(AtA6JN(=yX;`s+2{g@4jod6Io z|KoVb`A|U(Ql*fPd?=EAFQYI5vI5_^it6QufxfSn7vK&r;3e?_Zou~zU?d^SA$$L)It7E+*#E9YNIv|H-O|cB%1S6L`db(U*rk6rs(<44Z$=g68ww(0&mR=# z75rUN|3qgL#P9tu0l+W;CJ^~Weo%EF&_!N(KuE}c`u-df359}0-HV)G0C0AZdiPTT z_<_^|5*p422aMr&&It;kqyxmyk6bR2<3Hh%cLS#Ido!}@JF2K(U~uFW3Cs(eDEfJY z0b=*F9fb~1=L6`7EF+16f)f-1A+N~x?~DC@{n>^@7TJgVBFE+d3ke_-IDc%?-vfq! z6CGsl{|(UrL3trIHugZK;)iX9^L}@*tSy~9>}~D5Kyab&4c}`*uwUIs7YroC3$e2I zu<~}caYFe0i(yBS{;wiwq@^P(Ers&UkQ>q8Z2R{>;2*;!z`6Lt2L0}v{l3-zkjtM^ z^SA5&Z~B1^{ZDNF9z*>b+mXHhL$?2CzS&>5`#*_grPf+zynWP2+~ z7h5Ob0S1su^+Gu70sa#(f{!gKengHAB#15iey`bkdIIT<-&zcQ%)rYF41(OafQKEd z5DSQfvm3(0)566XV(DRFg$gLXmr#O^Dmo&7tg?;Q&+_*UD~Oe=v$F-n8iIhJVn~P$ zV1j)R5F6l;3d9a#=kI2RaDmuE93f5+C*Tb$5NC)B#1-P|f`GU|+>p;s0N2#7Dl4-$az zaAiYr0{N;Iz(gVS?6+his{TV*zQ3yF_cyfw1pSc!Mk*Op`sce{;6OH1T>RHdT#EJm zb+q-VZ!s(_m)*`>-zXjTuhLEGva>gRG|>V!dW_EZe3HAKE#hM6AyD{kkD>64Qtg^{HR z8z&``3aSrUkK<`G;C|x@R({GaX(2Nc#jV=gzMC9e+Z%7qR5uh zy*52?%{`#IYIPQ3B9v+1#>Uk__sFb}Yw%n)fDzIXh2{0T=`NmK+U;t0)PsL+tH0H0QhJYl&G zhZOJK-HB@(I3J^?eMekJCjIBsh!UpSZw&fKyjCCg4;*34qt7+`ynYt^!q#MMV4Xvc z6aQV%lO(DY+uLLX>qK=ck1qB+AmpXq@9D{r?J?)H1Rc~ZWra9Y>%65;sBsE{i&|Kb z-&B~XX|cM|i4i9j4R2w~S}Iw(8udu95I!lC(I63IS1h|T)Rh9N};5@=`_&8}Hc&9naTUuy% z%UBzEajs1 z&7lYMm=lr*OEtd8^6?sn^YvqIGTvJHh3TG}%r@-1Zn%5OAGy2wP+cCd3zJ%d2~$3)wI6s z8!nG-d)VC$8)3KwAt9A)cwfyRpi;wU^@YwrlIz%d*7-Q={$V2AJ5^j-KqDdHdD*t^ z5~b~v@}be>3-%)EHB>3dI1}G|H@9yI`dvJ#bz$?pDwNP|*HSwEprp$p^2*VYR0(GQ ztApLiyTrI-HPVF6@gsi1OFhkHGG@=+wZJi_q(^gIXIK6AqTfVpiCE4WJsTi%fBpLG zLW?0$cDjjb!#%|WKjS+D6Enq>uJn$}=x1+i_%16OKIyc^4C+kuv4U!Rsn>15*R~Kb zqY1fjH|o?yU0U4Ea#idVnX~DKi#>QPk?|pS-X7gZc^e2Dul+D@RA3h9FMROA>KQ@c znqWX_du9Uq>xFy=dkSiG*Z2S~>-9+G#&)X9O>1kW&mySW*CMpnd;=wMG(HIxdJ@GJ zJgy&!kb8WRZ5sv3jy$bCKb7FUH2U-gALW&gA2NiUGZQmh4T|-pcq&e;=Wei$v$ZUi zJlH1tN>t&A->Ah%AvL@wYqad=rW)PxI-s2nvG<9wDj4L`t5Mtfd`#oLM*!5CEBG|e zaG(Uump(WO$Hs3`HRkvb{*vT{@95|9lBBL%?>v(D&Yx`)7at58U#QD(OxGTI;+1w^ zja#2}X-`;ITieu>EKGW5|MNInm>*gi-Bm~57x)qaeGKvHRQn$=!%n5l-d*FRj*^R; z5@pT#NHnIn*es|J-cGOP{`lr|ZhLH@|<=h^#XvSf=?beCTm$ekIP5mYn&XaH~kybIb8zEx5q&-#d*6=~9>n8V)ReNeR1^}@=YNt#&pYoVXu2Wgt@7kFn2 z64>psy&}gm>I5c|N_^RVm)^!ak$i8%#>viMF(rJxng-|N$NWsLob%pne`9`uFC|YR zB5dFj8V%|F1ob-4Jm1e{UWF_jf8tsSy1qnL!Zhv81|^7fn~gT)piYos#g4&b1;vD~ zwR!T+rcAJ=^)HWwuRL|8O=!?#Ufi`aqRmRL)i3UweHf;qq?=(;cDlOT=^4||)HK1A zwbyaaEG+KPxSp+b-h4V-V$Eb(XB4r5(IZOk7~p@&ipL=yd-7q{ZP)ocA)`;?FSF3r zaq6xGc+qZCyAE-UW?azK)pp@}oAC+$q>1t|1>uvf;|&?Lkww<^XQN3c{)Iz}wEZh3 zK15}UESVKp?2}?4ippt?u18AFgZ3f^7W6pzn)DCN%-WY9JHxLk^G`%T9p^NPSedH* zrPgo?_0?!Uxwu+yiV(BVV0|>%fB4j=nGGU9u}D}US(3Sh54MoryDbqeNZ(TO%8( z@TreqTct;qO&Gnn<%!o~`Kx^uz;QjkeVlj-MV~Z=?&J7jo4!V;J@9*Ju?sF!LMscu zCE0QT)0n<^ht#ASpOGmy669>*LuIqoUD)SFxivXT{<&+mALhxRqk#xet_|#q)YTm5 zjfj!t!KmJG8%g;hRt|aWykP6A>0Kr-Au?y|OCtYVclor~_d`Htt~wgK?480P=!T<* zAEkdijyfi1XckPAP@PDlj4wb#^W$QCWXY@C2T=Aa0wn}6qw1p)yGTWXvrlNYEv!_)}RVu9y zRJ}j^?5h*DdT&|}JKL~oYx(k5in0r3Pcf!As2U$(m41BvhSr$~< zF_>tvFuYjP8j{bFe_@#zDTztM=ALitcxZKeScIaE4mvCb`29OvWW`dl9+`C~$f5B}3+n2Rxfd}cR^ljJc; z1LK(Qza|K#yfcpf27H4&`T``-cYQ3vUhpDLMQ1R6q=ehrQq^!W52**m<`D%85b;kZ9Hv-`xb*=JAHoPD=bHB9GSSiTK6LN>{l-;JlV>j4OmS&Dy+I$_ zMBi7N`0}iw8{QbW{-m6>-0$m+)H-YIjh8p}BHtG+sB65psnKnqtj{WKFw$0be8iSx zY8hJ!r@228xXbXB+Er;4$KEF9QKV$r9+-%Ud?iLPs&R-ZT+!dAnEX=Q5v7k)rLdK6 za>%y2cP78C9x)%wh^zAU-t0j9ftvbfD%p$Y=r~hE)X1Y@fBu(T)Dz_2quhTBKL7q4 z8Wns3@2~{YsJwhYT8(mT>Ke+@&TdfZ{a7h`YZf|0+HfBMxXqGK)m^< z2op%QL;i>`p}$3#2p|LmB20T%>pul)sKmw}PaS!Y_5XU1#wYMwjD~K6UVMg*hIs)E z9UUF#`%`&j@p4?qSJNW~tT+OUI0DSn!)4N5l4ry%7txS^7zlfAG&DIhB{X8xooJY7 z2(%4!(AQ|9uX-W*haUNdV)^KY*!_o*k1-Ad4g)DF4>jTrNtyujW8pYQ zdZNRQko>QZ{6o6e=!azOPoH5NjvrxA+zZMK@OQuI>YWpoo&O-OnC@8RB$Xn}J1#gb z6j!s>r((7IkS!@aG%o5^Y;<50U8ub~R4Wem_O0Xx#aUH(ZS=i|{OLsrX>oZ}?G7c@ z5Qk&d$k6n-b@~Sj26jA7XA{9NP9!lzF8GxHAS5_fd2y<_-R%zHOSz~hI(AcuV0)58jDi#w9 z0)1M~xHL5;MYUXeLG_N7m!>(-2QS8Krx+El{R369>uryth%>!4$;jpoUmY(Drk(E} zp9^00rR-gBtDO_~udOKcTWzKn)=ntfZ)IS?_h@=^eS7JBki}7R_x|M2JJ03X>h?ms z=i!r@6&E?4tC=qw_yl0~_J}V}cx3wa)z&_tyGGcyRMMNzx#Ov^OHKM1@xLg0>!7;Q zb$K|rOK^90cPDso3lc22ySu}N;O_43?iwt(y9IZbk7Ulw$=oyde&<)kAG~YV+O@0J zEB*A--HY(O`ZfZ?R>p{QP`_ai`n!l`jpFgpdEU>bQ69$+c##{*iVjj8T4MCfXv3w4 z%vjs5**UrO&EVGI-7LH(u*{Z|9XP_8pZewwx2(`q;~Rz`dy0(@h**4THC72q6rp^& zDQi|unUj2B8Qqs!u)uhX6>G&=S)WJssR8mU2UKkzC+Ou>eeqN|XYdkI&gX-H0ME^R z_;)7!^glitd40FK+7ms^v@?6W*xYBnqS2;@P@kc-Xmc(?vX&oMUc5lre9+rI5+#b( z+W(e?RQ7%1ORmH?mo{!QR@uAMmC=j&o}(z@hOy<(GRuigqPx5t$Kr!M5Zw&B*P?+& zD-B&?MrgCtltM1eEt;Trs9f6!@Lb0*xem)nmC|Ebs>knjtQ!`K%qM4WCqe1+PGIvT z{ZjMrqi?Kg6vBs)-IcoaI%*&mMC+5{YM|@)Bm5}vL*&gKZjhJqmIm%gD=KojGmIvv z5xj^yTv}1@q0a`^I=;0lX?}|y&?b)9MOSGDp6!+{qk8)o$)sP4 z1~gG#N?<+AXNdhrN>~N|V4-z+;Es5}Yk^SFovnjtK&08?5lNerO)a`5ul&YQkSg^D zPz2uLUcSmCH!spE+aE0+E)pn$L3giVQ7ECw*g&VsaDn8Sx<-l10tMg}D)e`tRq^*Q zV0vuYEn5*Q`i?0fRb}_a&FYWART7g^g>lgX^NL&nGC)jSGQHYF`;~EnkMb$87rbp+ zCP5#lOt5E~$$YckbxAQ{@h>{>59?^&J+01qG0tKdFDQl`%QA9x+8{r$piH=8cHu3y z-_nQ8C3eP!ixX_jEn?H2MZL2Zz>NKY&}I@hJ~Fqgi34b|=-pqQ7+zDChYpofw#R#X zcUF!!&^nI8;3i&!{&C&6?$!ueGfF_e>saksPuKOmZ|8m~7h_(u0Q&05R5N+M?^F!# zM)9RGYu+hhvX)KRr+~}gwq^Dw&T*Z2?L#AUy8qlOe+h&Bo4xWsxqN1V!v4FUsD7WaRmfJ)OkLVyk z2msQ{&)3^4CNMq_|1Rqh@RacgaPkfH0|a1t$NI*94F^Og;@y=$enw4A17u`40^ISR zD!|c{pOuq~vUmUa{D0}B{+s9j4|1zNCjir%(}3;GjPP4Gf%V^L?*DEk zyq$;tcvAkn>)*|UH#ydC&4gd0zd^m9SN?)}KPS~+6GfN)_ojd$z0vP&0P}zG|JMH& zF8#sv|BK;wpm+R5=ey9m{%w-|?7;j!$$sm|{P%4BoBI2Aq*$loVjW|E_ad}-rT`6{ z{26d^>qEEh4N+2EQqElp3EAkq!zcMeaD0MHdTLp0DRq?Iq&%N2(Ub0OCqLg_dbJF_vOCh+uGJ2#{fO+Xsq8r4L5Y}Emueu&? zRr!>nvj-|y^u#tln+?nrQJu1zj&~ZG8}W)(;t`DvQM$waHP&(aZZU%fZIFv zmt*1^1T($x+NqL}+Zh;|7;;>;=`S7Wr>v%Y#5W?%NY?ps!dNa32B-5O+M5fbrXlq# zvh1{8`>+YoGw*gAGBdKEorgVROm0`vHAxUkFLvrP+mi@>I(lW&(l=1ixDkP3M}U;+ zyC2f<4Rg2-ffTCxkmGMm;dQo8_#?DIUtg|mVPg}PWR@fiwJMIBg^z1)okVjB7B3_D z!ahP61dt1jZCSs$`Gf*x4O+Vq@F9J5j0(<^pi14x(NMatC z@g9Jz@7LE>Ch@n2bggR}k9QtpW0J$?^;xFH!ovcbJ zgl;L$7mD65z;cRBsawuLd07RF#x z12(y^D|7}`nYL3-2>3%ozEW4kr1kJV6R!uTVhORj`ia5_DXkP6n}xWE(v^o+#99O% zS>!(GxUis4C=j*{a){(Nj0&<|vmy+;|rx{Cr(6KL$7R%-}mw_43HUgrb9LsHt5`0Fv+Q(&vl$K@t4>A@Qf9+ zDS6Nb&T9zKR=q;PJ0xuzwLe028TsEKlYiY?aMuawFICBtRVhNAW{>QQDb8%ifbY3*z;f`neQdcFDPuj=%cySA)5Q@tP@yX(a`{Z>Sl)Ff3Y;*BxWP@#* z(5C2~tG(Q3Bqw7IAh{pl6Y12~e@mZnWAX=H4F(Md@WrsOggtT|K;ncz2)5<U3^5 zaJJO5J+1MIs<(n6WteKTRpX2>N5Cnt)`mI(jsb;dADBiP%e;MJ9?Is#?K|Pe_X1FM z>l|TDp<$Ir{=w8TDhGx1#p1JpM_s)r{fs25L1YkGyN2DioRdywOxOuu7N8S*!i|h+ zR~lzPwi^_>bN^+!&t9c%Mx1R(02X|ZGA~MyP>Y_50=!mgZf#-r$kxATH%G^U56S(I zPeV!(7%NJ4OEDN$uOE@$hAjaK(tycBa#j>Y!FdNMJbU%S1$^8RM!Ja}P@8{#eENu| z+0lOHlJo*=l&`8TC{fVo)!D{VmPSiJPSHfPXpt=dG_n`Rrm=J+A$!jJb;l(A!`TaZ zV@A@RAx}!lYI;Gm57IPU4*hmbJtG?orBJtNyZh~G?-(G>@5C7alm2AJ3AnqI-A3K( zU{qPOZdgE~=JrhT-Fa@5f5VT+oHV`e&Y6|{bFgY)A8SQ#OoEEle5E-v)Xc;Yzg?ex zn7x}D3tF1!VE>D}{%!n1&=PdIX|B7;*YhgerJSroVf-wFm( z9NQAID)x*Nv(Tx+bL|aC)6|6cuR!&W%`wc6O%4w4{cW9GHxY%5pqnoePV)93$%A~M zK)HYLV;+C;9WW~?D`Pe}^jA99o533tiO^mThwED^Wm9N%9zC7&24;b8<39?5{3I7N zt*w}0wV23T`-+o(&e*;;RnHy!JPJzJ@wSwEUbhcm9n=d&eIvP+aZfnxO~<3qjp=w3 z+B5R2djfbN273Z>Cg9qvCz-Zk=II$te0?WXM9O5Wn4*!?I5X1w3m;hAgVeM=?aD}v zm0ZYBQ#&i9D=Sa1EzJfGpVyIg^=`gPjlgNJoM1%_5zIzHXW@l?yeV3#HjL6fGUD*m zdqhenDYW=e>(a(HJmpkL4DEULqbIp?5gO0WJ402oo4SOCS5CglOtlLwGDkhAm0G{S zO;f)zr(|fHXSLKyQ5403N)(spn5f;UGY1ATF}#>jAv=!yo+r|0SoydFlA;ug`oRY^ z)pO~hZ3spauyUZ2O&XW7U4xUi?#Kmi6S^-}u$*!I>hRiX!;{b@ETe;~NZ!hk;s!Ow zehu*&Z>{Ccz|~^sOv)Sd{s7Na*Rha5T?GCVH}K_^a*Db0NDz=0#}r}bR`GIuhmrZ= zgI3*v;ONEDi!@pPd8*Cq+1}l0MommjBI*Uyz|!>=bk#s=kcF050q-3&fyT5s3l`i6 zem0s*ZVhiL1_glsQsWxnb|CS&iB~fveAYHr8P-KUuyu|jk;D8A6#LLu9htmv4|aU_rX8GIFIfpCdKp78#rNcC=0$B+(KL-0 z3es^CL?75P4w!lwx8CED+rhHju51Y707q2~oyKeXB`^#@WU#8I)Xm~*$w|amc*_8x z!pK48e0Y-_Jkw4B#u=I9IOr`{o}hql=fG?yRo3_1Hxg8J58y@VCU=Wu^7Zhaf?YsW8SFX@zIlv!WR@Mh-D*PyN4f7C?2^7tFKIy6p?C!Jl)g+(Y8lIXKexZj zr|9KMev0&nX-pb&Xg-EF78O(me9AAG!5-B3ddfaqB288}8hyW$B@ojxl*Gjw(%zkt zq~#1fu1_995^=b1+2a1C*W{85Gj63$R|4~SLg-;m11b6w5z;Z%G6J+MTT&F+meCkN z@awz1$BCW)tZIHqUjLh_=AV2Bf0Z?FVpA3l_BRrc^*`&{w~N2mwZDdc)wN7-M!2p-#O(ji)h#Q-?*jP+J-$2{UDJ>rCW1UhB`vH*dZ;Ymri*fF;R zfLm-plXrtpBP4QdP%0obC>0WUzOK%?5j#IMEj!&k!`i~q$ItTZn}a+&0^PBr#?!_l z#vv0R@;%aQ@B+cD{QX@4j(`tYLQ%qy@UOs}GVgjF?}XldY~(k^YINlF+pOC{RNVsI zBHeu7D4$p_0Hmvjn~P0;V46REolCu2t+Sr9j+?HFi@$Xszy{JK$t^V_FE`;WsxY%8 zvp5sr8SEMA>C1=_>Kp6>@PTwm^hi%mj!O;4L!Rh#?Qh4bv#PVGvyKgj^GyIirY5DN z!#_X=%v@D*QeB_rA6mQ0`ef!JW^bpY;3(;-)=T{G;=g}ghXENO6~2y z3Q2X3a|b{=dwRI|eDw+Q#gAnS^Ze=w@Wgzh0YKvUe^TZ|(TffLuwZ@@g8rrK{5hZh zaCH7#RQMkzkiS;Tn@*SWO>N80_zx`5+r_`FmY>6auNH>4(La&^j4Yi0W4ZivQ2e{n z|J5k^Q#L3_FHA2&FG?>#|B+srUWQ(lUXK3FNkgwhuS~DCI3b>)v1~&Deg6|5=ORN z6DUu%eXwvkkh4fDR+h4;D??U3loP?B^cy7b6(FIq`ydp^4g?CtOcMDnP#zSuHdNWH z0Nht; zW1dPP9ia}xXZCYRNE)Ish-a)x+!--9gule9i9R=&#E8f2cV=`oBx)nv8p9yXA^m~0 ziFSGuKE1Xw>QVGac*_^@naOGael~n%tjX?PI2}J5`(kE-RCwt{WrK6I#%MmJ$MZJy z;^8F8W;~Y9&hoBnLmT1M!T;m53nz1zPYTXvHI;;)osSaEo@SR3`r)M_0hoRA5ew4n zZJX?5f93Q$5cD1u?1*IbPN0HoxIhHn0q%Ke$rRp!PsS{iTsFB7zNIN2nN6j!CccJV z2RRc4S`6L8!uQDUv)J!{)|Svy6;^L=jv`j6iWEbz?eQzr*V;6(4#vZ!Dq(N_+;>(& zyfg3}4*#sT8@x!D(nGH1Jhlk!=;|onrzW9zqY+rOvg0$i+mCEcoic&Rm+{w?cajV^ zn-duUc-FnOxp88uWj+Cj7)TA#G1{+bq+e$67)zh-jKI`VP_?pUERc;pkvcS-PgoQ+ zg5B8f!s(UEd5xWI4+rkwycGW|N^=&1I! zlaZsiI%r;42hLxZ1hmjsS+I+n9cXVSOpY^k3TM>_Ka@K;u0HDG(dgVQ-G9SOpR8PH z4PV|zlW@DBM6hO@;D~%nJ5h?Hvy2Ek_1bJ}?LuhNF4%v4H#$}iQ!VS@{Y1DJhR^&Xz8F6}u)2fmY;K5W~%DD%=Q;z!r zM*9pQTBDfNsOA%hcN5gz<>PTHBKv-K-G>~+ZP=P={^?t=0K^RvSe>$a*<{Q2d>$W( z`d(z>owi1}xl5JfGL%of7GcmSr`RqhCt8B4=7TE`nq2y%l)(rouxh(JIaSpP3`w0z z@-8%2ja|Sv)oB?oIovmLqEST6x*CGUK&T}hE+*&q-$!q5@a(^(V17XgOM>VE)nwdO zrt_^IeGK=1{<8=G>WROhPgqyz4XmE8LB%`Vd_OFDQT zcI3MCj*dog(DPW$b7gpC#jWLCWBO&Wm;HA=C6VV{xQYqst3)l{i*b|0=_MBEPB159-vf0lA$)jbHro6NxOb46OX1ySn5p?@MDZZ-G36Rj zwX5)IGq^10!@*-yi+d;~nT5oNkeED71GB!diI+*LA z!9I_|LZ89L;S-7DLH4m=N&}nMo&11Bs++)>t*cyzzjBBW|E%+z0UFDtWYR+)OR_8A zM->Pr0iIq;=C)hbcS6AQsCQYc-@PnHp)Q2EGP5ytmG47#pualxNibFD9c~c^jGN12 zpJG4L9r76oBuf$aJ130cXcMhd=KUIGG9*8QsBC48!tsD*`5TqOTyJuW_#ZJD;7_1R zLJ}x4Coy;W1qC8zlgfviPpf|BnIp;^wlJk~{R_A8q$l!u1KJM0|BF9LTj*4njNMrLW{;!??;IIZ0LFS%MxAHD3vfJ;bypUfNpF(;$FckZQ1CTj0b0e z6(8~La7GxgE_|qco+JaDqss!ygOtSO14kc>g9AtN3xSS#{X3mS)|QUES@dWdCk~`F z1a=J!I@p#OBlx}P*Q!{7ZYv|h7V-&_T3pN{)$BSi6gxpokxt^E^!v zQIydvTMds*o824+6hblU;+y+c3Wtw&bQ z44)d&QENon_Ia&rgI;b|2O_!mO{AP#3e`4$Ef?x`Mip^supcrq$Nzda*|6;b=5kdq zVwSGn@S3~ej?wNMJt|vU++&MZvhZ@fNZq5x;Alr6*D-2)%~V~7HJ9F@7%q4G*~xVr zz3~jNJJq!(HvFm>F6kbW0mrX8hlMR^5$c1;?!r7y67DVxy}hzRZSa zo7LP}Ok4h06>9mpM75$Jzm}>5l~$V81(jv~l3*Zn*06-oPl|4gg1U61f^OV+zMlM3 z4XYBQ1?;Fi5c|sbX_<~$qeTM|FDoThHb+y8PvWNaK>ExOw-7;?#?=(pRd-fLTJ!f* zN7FB9mF<>rrP)=old ztCE8gnN1Z^I50AzTh9;A2VC^}!ZjtvaIeC|8!Z|j=M8N{ciH@zr zyvdMk$#{vAoy;2zKcq6T;+WRvu$d=5rN^Uf`bf=2_g?jU8*I+oi@z{S&=A+ZsLQ!u zNqDQ!1u@@Xv6XGH+ODt1-ER^JJttH)xPgr0z&svYbth}bLp1GH&8?fX)z*X;Y}@Wh z`D$aR=4)Ku(pcxcd`8;+Hh8-UX$1r>Vi?v$Vg?J#Q)WlD0VXV_n$Yy({6pDsMK=Y} zbsFo<^+^ExCaU3aQP_Ai=l%0ysj!;E`*?q$WVz){X@I*^dzzDNTjg%pNpx19TqC}{ z-!o%n2mda%^sYNl7$;}=%GcurA~zE+oQs)={rpHTcz*hp9gQ8=!_3H$x^-U_2>=|7 zYgH$igN)PI&ZAs?LLrZNHBzeLVz6SSuW7!V)puVkBu>eBM{#U&|GvRRJI?@_heyQ4 zM<|#t1A-DUW<7F1u}a&?MT=BEe3>lG{v$SVdPZbmX4?XJ)?Au#L;>VmWF4HWk+5|e z>Vi0ojj6_28Uiq%Ia)9IhkF?wd;@W^A_Q()9x15NZHw0la5m2D>fe8D$>y1?6zRat z)&Wpn6j8hp(uzXTByBW(q+>fziWeu;`1&2+=Pjyz!Yw0b3t)GeoBBB89ntpCiWG@f zH>K3g4l5ef^}_f@BHvY2_Qx_P=z@YFD@iCS>;CtZb=(aRVDg5IC<~=?!gQxHmRbi zq7`OL!&L~<_0?UXgUp;bdKuwqY9zTV@!NyHm^)|59BBIVIIpzcX8RGmV@qAMX{>o1 zj2la_NT3~UD_;`Z2Z6g;UGWlC1LN!&qQOFL#GZ zXc~)M0;tk`VrRSR%-&TEz>M+Z6AupZmanlYyZdo6Acn0GP*TD#!wIC_-Dj7NS5A+! zbbnW2Zx3bT^p%B0+xz^%z-nYQj=;ZlNCQObOGJ5TnAySv*7@pUoSIE%Tl(Gl$ec8- zkxa`z5m5Y!vukNz3q(+1X?Y&D`8NHrDFQ$;R92iK!itibOHNK)JBBArRCv+NroKM=C0VsE`px>mB@(lWcom-N<(@ZsIFA2gHczf3gq1eB%ENUH2cE1OH|p-t;GLHga|bra!ql<~N_>zZ9i! zSAVA;*f`&4h2Q9hHwNyX>4%@U{f({rJN>}&lhpW=eh_{m8h+9YZ)U@PU=iL7hQCaN zCeFVMgKvU@|KSjPixl{~rr3>frFmkeS{zfO1DO)HZFJPwI5HN>|sBxE_SQ^zj zl$40f7Wd73t`j-ecrX9$02m1o0NfJ9FA|#1F2`D6iXJ%(8njl}VUo+bG zX0vB571QIY*_;)J({0VgDI3lf{(5aM*Hg~hkq8(5^jp4hJBe;19Kq;Z8vQSKPwR8q zRzP3R=`I5wyFWmaJtVH-$+r0ndT&VVkt0{k#exu;{Af`=cSAzD6+K#e0d(H(zNQke zAv1@ReE>bD-Xtc9{UlvVIE!=`EYd4Vlz2zDAq$FVg{T;ODpd!GPn6&+V@as}l{)tm zRZR2g)aE1e8qb3}ab zIMCg86VNDkC~X18Fp1DCnbe5RaOr$z@5#JfARyL0sOSqz1!fSgJ)Y{V4q?w^(nI6} zhrzGnd$0yxxv*ykQLsSlRC$?rJtZyB?2q73z@YvZdn%S}XgdECZFYL$(eZI)5A4G* z!==@EMhqgWAUjK#F0_1)S`p~%d|w}1bvxKjo!owP<2Lq3PE(lz+QB)K7?}^4@IZc) z_wlrs+JIsCQyB{m%^`Aj@?@t35vB6#E`qJ9>$baMdzI)YW|Ra-F>lHs z;+fVCjJ&EG^OnP1TGKu{ac~euA^i0T=cP^2RA9e~^)y?Hbl}bwBsV;4mE^a`K zAk-gPG*de`#I^*6scI)>*fd1~qRD_GlUb8GA<=es>iP8+!qzi3CGH?(_u7T{a4Sql zL^A17u1skQG;yn(AbJHpel{I=v1|nG(1lel#T;$*D1{4LUv>q#(S4H7=@s@uP-j)r zCD(T3k7~rA7&D9-@x#30UGS5oORZ8dfuT(m%}|3h3G2?QTF^8|pMt8pI74t6U9VhI z==;ob!QV(Bx{+vlWizm48f%+mUl%u*otD70MDZbuwUl}9E{jd)1opG%`uAE=_RDaw zCE7Y2Uj>TqCIP^-`piM!U`mw@&`OvG;z(pi6mqSH;Gp73Lhwu2>EQX(b%yq0kO|R3 z1$9ICqnfs?OL2&jA`6zHV8h*3pWoheGahJwS*1gk4M;smsTo`ABm*_Oq#i=>XmF@b=>lri?!x0Y>KbQAeOGf8wpHL+^ujwtX+ue`( zSjh=UdOX*L9j;zYR0kMe-lRs0d6${m-!N^S3~|E`a4 z^BhxG5eTb3Lr$5!FP#-*LUyDBRx|A029G^dTK8cp<(1y&fY{nNaCRlGj|PEclxSc= zGeFc@-5mPbx2MZCl(bZEP+5+$+NBtuU15Q5@azEyqTlW|1t( zS*qf$QVE|T8S@+H(iq=|63D6+POT5he^bJtuHPSdK%z*Rod9Qz7LB=TA(5umLC=lo zgB1v6hfOHthP068B`;d-LCNV=w5T{kee&?2Mwwk?{x(sT7H^ueHs~AYAUma4@^6j zjnHCW@mphbrf%;m54vk#9>1jP!q3FF>`^|-X!i^6Z zsx1BB%nKFbaSVq`hjjd-AaaU3pzJ+tljd@HWonsgTCSiV{k|YV(x`P-ZP{1MvK-{= z0};&&3{|eIOO0}pDZmwys@5J3Vv?J2b&z>S5L1QXCJ{<+vHm?ZtEq*26&a{)o)eYO z>?D`_*2Z&}54P}Gsvt6OkZ0IHSrRjUc~Rq}ZS9qQO*T(Mq4ykd zK!?`*_OAonRg>%>9ukjsZ<=dL2g`A&Ufx2#~x09mvQCx1Y`XGhkQ{8@sT^ z@W7B#%UZ+y!?K(6Y6}y-l>EGsQ%tX;%Ofj+GNZ$aG-j`n%Mmxvj#CdGSE$zBMb~7 zi#W%l#mjJmKOa$q;~Ohk?<5G~DhO0g;MR`5QtrQH7h=MIx%$z&>}BQeNsSQ$I}|7+ z4#fERo0rZ#Y;q>hnD40bpjoM~xKCW9l9m!U+P51m95&#xr#%w!%hdQavnC*mN_5Y_ z2cL-$;Cq!7sw{CXR+5-o8`I7#*G0AM$iAIHTT|j23I1LWp=F}oiu81Xl!r&87)Qbl3GM$=KAJGS%Wqu@NP<^^9yw|~Io8*sJp7bBiY#b+85Ej1g>U_t?@A2AH z)NEnaoLoKbU=%IshrXNaqn`6hbPaV*pxmFEaE5B`Gs{935B`W2gN(FjU2naFRd282 z4tg#(2x_a=E!_A~AcEIljgNlAfQW+6RNJ$JYjUhU6I~?}y?{+8+CPVEjYLu0c<>Wb z7;MK4j!f5tmDQ$P(x*Y85Ll3_#%Z{qVvV@PuOQ0scQCc(YcWcfbiJKSHdKgF;?)r~ zPAMQ?Os&77Zs8m;;^ZW^a2S1M{!lF_AIif^^ss*Dz}%Uz9VOA5QA%XP;qy^|STx(4 zZ@-CrEj20zWPyw{;UkH{2udPIm-6?F3QG+;P`N;Sr?g`}*Qcj4T!;;x%!cx$k=pHe zL9k%9%4td^s_I^!7e@zYYPX zsuOe=TnCdD9%v)!`WG6e=az2mZ+cni+(-!(5+t6x&-D*pA9i?FDxm0uR=hEV3NiHx zF_ZV-`u3h2zmi&inF-yRRovHzd*74)4xd zQGG6m%)6_2z=b{TWHxCX&-o5~-CMYtlPtJHG-Pdy8@Qy41Ea&-iMI_00|L!Gd@C>3;8M^#^u1;#m>&5uXr1~(pB<$kEJNITEAG{``U6)c-nxK4x)}r)(`HM zDkOxdP*i_U9?J(u#o;Imd`>FfU+LRuDemz1gx?JM&b7+oxo~$5e%=Pi6~VAGnM$&I zj7X1hb71T~syjqN?@VAj_y9L5e{`Q`a$f!rcvZPs)m^(|80n9$EAO>xO31 zh{a1Os}sxm7A3Q)7L*Cc1`cv?n?qx9^pvNN+b&40zSe>i`DqUiG3C#!!&DP5B)4a? z3WasMLitSNuq|C=NH>L7n#K>w>|00pUJ)O^MVx-)D+YMqQlgg=$+2ZwxfrPZFgSC7 z{4PpN(#bU;6dlkkK&_+!bA=KnnuElo%j0U+jPpdcWmbtd+r0_FSO5k~@x%Az(y<@iWJ^H=j2y_8~6>SBcIj#7=SEMN?NhU zP>Ttu$EjoL5BLsZp46i38zp|JBW?XfRgHqxsKOpKFHcJ=q2<)gwuGMv_eH#zV#C^T z{e3W;*H6+vV@7t&=noF7vW+CAHHV4brC3kPzghk#O)MMgRZgEPXMt`r!<>^6LJYTwG5Y_FGUwx6c3+f4%kvVX$AmyWD)ZH15_aAd~ zlPdUV7`;$i>CxdkMadSP^F{%nena;9=Ba`LF>xeq8wNv>ajXb=9HPt6gFQV!Q`>V9wjV|EugZZp}me-krQVs(aUJ6 zEEf8Ug{gsxB2sVY;}ihETk4Ow#E@c7%79-0?iG3zmBSBJZC4!-bh4~HfRxor#vJoW-1G5yX+?9ov53_X^iBWw;aa27jE-e$XLSo4#K?u`9vYRAO zoP~CXM`o#oa1@%;39<}e8Duj;Lq#(<#j!_P<#$JGD=oM2KfelYm=;kWJZ~YLfWKM( zF24$GGHR;wVl=&G|zhM#NRBb9U- zJw=6j`|0$#LI%qkopqLfBBE#12;3d@RZCAZmAA^HQ}t?7u#dv_s6v+!nH6W%9$F#h z{p=v~F4CBT%~EOEF2Dck=2yw8j(7_7tZx@q`}yN55R@?mU~^RaAp_qV2D

w8Of| zIcI#$NN}yhXT%J)w|~67H2Y>nzun^WR{NMr?BrqyuaPc$Z-2_(*(^Pc+a`p#XLi!` zxsm#Na^vTdyGExL)Lyg40x^Hukl-mQeOifcLwR+ww=3B)sP6i*w-Z?O2!Z$Xg$)r= z|A1wG=J@?LB%kE}j70neWoh5S0BM<683{PwLQ~)3TK@sevi=>+{v7@VX5a4o-@xo! zl=nY?*}sTALHa-Ns|3B|o32Ri7mih-SN%&-r1#Td^jFRv{T~@&zvYnq3RC?VMD_-H zfBpTLNA@?Zk?F5Yvj6`$vOiF=&EJy#{u=xdS@tW0`Hz499$fbK$g;nzP5;S7{(Mru zL+#(5+<(tSvNE&&t~0Fr1ocUAuAYxE+Ah_a2fFMuRo$$tW|K#`uZT*WJQYj{90Kx^ z;(a$_G!3vWo)D4{1~66dIt`V&QAxd4UY%))%3HJ>?&6Y%wcY9MjYMr-Tf=Qz`zasr z8ic#saZR9C*{imgP@R>S1PRi@NPv`BQ%J}4iZ8Rae=QlOpb@3LWyZ>_v<3po9IiwQ zn?p`-#n79Tp^I5qsAtz-?86u!8NZFt@XJwtfK9vS3jl=8O0C}EzP=MxkXkGP^YJEk zh_?;A+|5dEFRLdo0tfYU_oKX(BEG_NQQtK8G?FQ0T^N=)Z2?aa>a>n2DXYJ_NRwho zQPMP)DH?04y3}a?uAE(w{4~Tgk0~E(pt?YK9#3Jww6p1ZR-XfrDkUqbWY?GjDat}z z6k&@jE;-yHf?}ARj}Cdwio6tXGm4WT$wI!li;7qh=n~c2y4>TA4Y^Xe5Q_-LUPDDC ziiJ~R)kD=hu23FnMMvw4x=vzhVp0QpX~5iRr##g)RZ`i^TdnP83FS-8_4bPP+{-Iv zk2QF3yhb-P2ds5-=~@U2P)CL;-?a95>zrgx2Rv#$%5PlOi5%pcHEo*?oA1IoeHWWp zVa*2z$VQl?{Q1i8%+-C!q=29&3YC|tw3iy_Lc_bVU~0os`3k1G=n8#_<+4l;me)kB z#1W`Ty^MThw4EWFnhDyDNbvGx-@z4r_EQnWATRi4&ps4I)d+3?pL3506DkUx0ty4b zaG!%3_?8*~UJ2zfiuB>F{YxhiKuQrFV3kRwSKxlyTuRG;@kB-<#=N-4w9NipLPmQ? zLapZu^>G~J<&ZFy{pj|4He=771z%8(!5on*SykCIe(hS*_d&=nXGf-xAQr4!%Uls8 zo5h&NH4=z(z9)RKCst|w!=qPquzCDzDk6_1am-D|O%rN?^ANY~Ejuq@CrX1}X05L8 zEg75!mb*MScp$uniE!Jb5B!dbUPbJ{&?M5ypMPR<730)Hiz1UEc`! zv25ku0Er-PY6<73x>xTkw43hsdC9fp>vf=)N=&rCau}@^zJ3I89qJtOGGg=ST`T`H zXp=*YGDS7w{kS6aaHcp7=Dx$}<;A4+P;?#ki}S9O2@D>jQDNkE!Dsmv_d!V|Q)Nnb zB)ssX1wWsp@PuPwi0^#0cb#<^F9(4TDK4LZ3t_w|ePNkH3V|vrv)&u(CW>5ak?I>q z5y7Poa!GE=VE15o&;$GJ7eu@VxWYf;Nr_fmiYs0wn2Z4Go=K?tQmmF9Ag+_iwySh} zuiS;NyK?efbu3eHLzcE=>;_u#Dd<^5F5erR8y4!N26St$6j}&^`xb+B3$dy1^7GWM z-fpuX*|fa$RKlFxuMm)!@X4(z4QvIx;>qJtqy$)0T?7Ze^Wt~lVVFYW7gCtMkD;$v zTV{784QWdO8Q|BtyU$0F7KOgC>FF7_wa*;gj-IM75P~G8mtsjA4Tzf|ROZ{-Ce~Bn zq>Uav!+r&xRc?-vgNr-+@ohCEe}(nlq1Dbz)_0oh;xn$tr+bxM9TA50@two%&%h2k5@UZWm_&VOdp2(sT<(8M00qOKpIvI_HirA zD7v39V1A6QO4cxpQ7kwh_Tj~5Yjo>#yGMT^icx6nyyz^o=v=1*x{N39-hCK-8e3nX z42qT^Lo5E46Mh~Lg*bBOUxv$TW$_#%PB#kqW6@sP5UbEf0#unM;&HMnb9kztAR*rR z!F&Q0`(Tb$7>a=(m*1nt4py%9WN&~llKrr zoBT&!lU#OlV_&t4C!_hKeI)mb@$j_+dSyflAy&*6yW7=DM zp_($|u~uhkFl({apiLx`?ATh;gjZ4PW9?MKny#sHr9Y6BgJiAurLb<1zs&%fvg0A- z>k@)0S=9xyk>L=3J@sE<(@4s~^Tre*<{KXp9hV;C8z%N~6!ikpD2b7#NkIXF;;(jN zy0ElHOQF$ZM)Mssg7rTXPufO%=&w*T;zFlHyP%`gXI%ypbybbKfi@BhflDTEXt7FY-NTk{Q^L!v}>sSmJ@%{zeY%@rGPN&jqtapM}<}xB)rx=7K zv?g47WfNPutr(@gP)Hh&`$#_;;de5|l}Kp63EujPiw%3^R`U`I673Eh(+Dzl-(ajs z6_a70Pp7_lg*20s$OTvtT7?ARe5xjb^-H6UT$jznBCm-0=Dz&qu=F7{ z@kycP2}bxy{@k#q^u^%aCNhJ0SPo;O(m)Q;DruR!#6~XQF2FU$lTa)u(htQ|MKAiT zR+y(xz8;*h&LwiTpF=m*gQ_XXXrZFIh&{7n?YTf_;p!B(pjxuI&qJ|-x;G@X<}+k+ zraPQSc%xGx%9}nQ8=~gasu(3))niwynk(f$`bHMRwciDNHw+d2SeQLT(AuA5;p|U? zRJ*v1L1XneAJ7Yn)-^*@gt90RaMCTn#;$FyLdFla$>FXRA1ubLrmr^s(Jj(HHZ5wS z&EjJ_cWU^cl&Rbe^qgk&sJ<=4^UQUU1{>2>>^SJRj8Pkaq>*1A?IztwbokhA9s zE}W!MHZ*0zoWbI=e}Z_A?Y(ejiJIJ%vTu)^;wQSouF^Fg8St2ArJMTQ#%(-@hA4{^ z9S`Z4@iPfOId;B0#Dbr25SCpiYY~`cG8+xl_D6qRx1<@J$`h!{vNYa4yLUm{ALG2f zT0KW}f8ltK_gK1*1oX{oNG!yf55)OnRH6Li9K;7;M}=_mYm)JdEX@!92tQwZdiu?4C3m4O<{RapJq zMB+Z5VwmWMK=b6Hm7`UApEC8udZw6&S>ly0$TS?ZC>d@yR)RmxW1x2r4En{&cPi=i z!rSma$bYr8@&L1<91f86Zt_dj8QC;B6g{h$#d{y_ReK*6AbpAI6Nbhc)5do$`I=LL zP>sZ&2tIvT1&L2-i@rD?T3Ee4F<2N$U=~)_|4Da)AqYK6rYSK+k}K~?wGfApeYeMC z{@J!eYU*?+;D!b2YbkCH73pZf_qr*CZR#)sRa95jE|J|BMRYzfWE$sGSu`<~pxV|1 zEO?ji+0{w~U0+cw53}p`_E4RXljzd6*>o&IZqudR%d9LW3##gd$WcX#f{0CdbTOGd z`bwd+U@mVfHsWz)Tk==(MkUCeZxl3K7wQaDn#&1NzKu|>#3*Vu{CI08>MPWCT+^C5 z(QWDs(yhK`sd28O!#D zYgQqiPJBZ)qWKOgBoC^ZHO~0{h62DG7}VDnSYZLr>v=qKACwv?j;t&kNK>cb%hyh7 zaXiNrV&O&u=-beDMI~%l=GqqBFM_sZF?4VR{=i_t<_bdrZUbbyAhTjuy?h*iuUo*| z19U||u{a9DhBfTa6gcw#wRYZdO(oj{w}FZUL7E5}5s0EBxv3Sx!>dm5U7Z#b{jO#vh==c`J zqRhmL%TCVKOU0@DWV(A-hHa&s&8ggkq@;(!tbx60i!8?N9wfM{-{@5;iCz#EQ;5zR zTNrx7`ANb*g7>?Z6x25h&Hg?}U$Drc-AL06?-N`&Q*_dC!NThf3H8e{aJIWeG^rAAsG7N{CpetcEvx^QISimlMmBdijF+2BOhg0nz4CHz$ zZ}N0`24QFP`AjkCwC?>>hR^fh(X>b0l zejt~uD6P!_-+L zV8id-rwQ!kcRu7A(vCC*xm+bB>K7We0 zDOi)2tlT`(?1JkQyvWhpu%p-we@#!;8(Ef?I*-yh$rI;^5y zT2H|{%HoH(oC^o0YTZ-+f#B#(W{_TXooslW~$(uj6kt-0RzOM8k(0Hx(>;x@#4eT6)d@v|xdTqyk8M79M5ua?l-@?uF~z#+T4;tm8oIiD!CUKL zt>%7>#N55f<*DR7Ea9WWcZ)`M|B~E1zq5Ic6~vjRbb^?ZekP@%%-f^9yE}1Heaccd z8&{6sle#kw3y5h)z|}=r<;+UUHELZOawF8vcQmx9-?^LGpL3)))IQ!%zPHm>p0+7o zf5yA%m7SREUo{>;_d?t=Y%{Bwoeide=iK`(FUp-;b56Cx@z$S|UF-hL+ps9N^fCKw zZCj#$eN~n9Ewg>fVczjsH%i`Lw@bKEREjU%+LV6%?S?jL9CF6+^o#!5dA}}s=KRXq z?bznDjgcRpj#$+&@BO|=t_0WB=(M* z!ppzdw<*2O*vj8U!8r4uJNs9vJ<#%w82EhPT-R3nw^?6uy}o#;#PRc;2lG#8FOBl~ z(7z$k|COqx9?K-9;2^i}L&>Gf<+eVD4xhZ&iN&_e-G!q#m8k9B(R(RxgX`kr`&uOd zHAw+G2Xg{!Ds-2t+8$6fWaNb8BY6T%t6N&1x3um{yZLM^eq&4PPN7#(op4ZH?M(?^ zt}^H%?*1A1j4Nwv#&`QEzBId{GQTmrJf|w+>BE7pV8!gDKO7%FZ`!U{yrgeedBq=o zmmzr@<$GrH4%D3OINxD^`z4dmxh?j-($Uj#b_|6Tt%`nLodp`t8dq{~Mn{XA{MN1i zUHfPEL{0CF)$>~lYX(vte(9gKviOd5nd46wo+V{{E+%_k`W=I?WQO{OpJyK&){<{2 zd??2vMJdG!?)qmKiro&{Y^n%DTN7yu>)( zHs)*I*l(h6r}}dOE1@XnXQ#(L6;?|)-4_Yosa@}?m%2pp6kb(o&p*oDQpWuFw!2Y# z)nB#KZT#~zrg-c|;K2iM5@xEyweb1bAMsLw&gAFb07N_W z?p7ikQ)_Y*EkIS9w4ZhI`R=KXqDv7iKt$K?Pxt>f&xj{KB34a0El_4myHUGFwM_o_ zu$}8aZlBJ{>hwiWM1c-o+|Ks(t9Nn{R`ViUj20@WCiNp;CI)M5-e8Mp%AeylyQ{tF z>ecCmJdF#4#)W$rC66y&?0BiyKZ3!Kr(@>lcy0387|p79!r!@MKgnv}_#^&`!i7ta zan4cQpT4xeN!~_!sofLabZIDh+x?#T(bK0bE}cCs#Z$Ala)sYC-&2i*YS!%gk6S%v zYm_^$9O}7~J(ic}oEby?*yqvvNUN{3t@+(rt#_!A1A(;4#f81LMf|wuu7huT)9*ED z9XuLhWM89Mz+&ODpo?&vtNcDz;*G4OkyytYUAl-MFoTb3&E>I-9&J z=J9fU=2C_$-lBhn!WLWmDi_r9^u3Pni<-IZ11(CMLOgYJ)+muL4VD?Goyk5CoWc#g zmHo0|Me4d=($?=;t9K_zu4CYWZepskvc}c(E7A&lht=+`ReTZ? zoa5PPA$8`_GxMe`oNe8>yqmTEH$hL*d*0Q2+qdM~wi-nU`~(XW-+CiP@+JFCkE zTaDzd#6L^ z0vyVx>X^IOTk60Hk(5YYFb{y(5s|zgekdi9iWFy|fHW*dBN1X1Q6LrR>EMJA2?Rlb zToD3`BBLNf2)7o&5dv6Hgg_XGfKWsvC{oDcP+aJiUke1^sK@}3D42pqM?^%RB5){y za0?m&XZ_I_EE?qJ~Rw!-a*Y95yjM1CE0ZKs84E^Y>NbPn``Tz@ zphIy0m}gED9guEmSPYhEh%qvR2yPGr9%E4mxHT9o1%ok0OKF0k23gI;fZYEi>mNa2=65@S z!-PR%$7M0m04N1l84AV(0*0`d6pla$V5nf~1P24I6$AE0*kOQkfgeTiGD8zj3)3Lc zL?Va_J18ZH!QVnfMjEo%97b4>26L-Vq&hQ(Lj6Pt4<`CrT~sdBr3o&V&Vhh=z|yS2o7RG z27z@MG#36K_+Mps0s)TlD2!xQu-e4kJ?sL?VFgDpGlIB$9OBV<9q0#%4TGrmwIh3|Y3X zAenYxNn{w6DrGYc#xP3CAOZ;7D<#9?VbHXs9+n76+YAA)v8>Dph6PLH1>*}tdL?Bf z0$!#LJQn8SN$6ogfE*b;ELq0?FeCy@be6~q<|`n0O382p7&9!P2izG(kV?oPJVs{B zu{f-ZufbVm#tn3{Oua@Jnf8L4I+$ZEQ7@n?!iOOxWnd$XjLmom+zv|Vk#I0SS~9N@ zxSUGKa9F%dpW^T&nZC!7h$QL0$AgLIC3sE(o*@pCdqk z4oA3vyJR}T+t}P3G9_7= a[j]); + @ ensures (\forall int x; 0 <= x < \result; a[x] > x); + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result) >= \result; + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; + @ ensures 0 <= \result <= a.length; + @ ensures \result == a.length || a[\result] <= \result; + @ ensures \result == 0 || a[\result-1] > \result; + @ assignable \strictly_nothing; + @*/ + static int compute(int a[]) { + int h = 0; + /*@ loop_invariant 0 <= h <= a.length; + @ // loop_invariant (\forall int x; 0 <= x < h; a[x] > x); + @ loop_invariant (\forall int x; 0 <= x < h; a[x] >= h); + @ loop_invariant (\num_of int i; 0 <= i < h; a[i] >= h) == h; + @ assignable \strictly_nothing; + @ decreases a.length - h + 1; + @*/ + while (h < a.length && h < a[h]) + h++; + + //@ assert h == a.length || a[h] <= h ; + + /*@ assert (\num_of int i; 0 <= i < h; a[i] >= h + 1) <= h \by { + @ oss; + @ rule "bsum_num_of_bounds" occ: "1"; + @ auto; + @ }; + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h) == + @ (\num_of int i; 0 <= i < h; a[i] >= h) + + @ (\num_of int i; h <= i < a.length; a[i] >= h); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h + 1) == + @ (\num_of int i; 0 <= i < h; a[i] >= h + 1) + + @ (\num_of int i; h <= i < a.length; a[i] >= h + 1); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h) >= h \by { + @ oss; + @ rule "bsum_positive1" occ: "0" on: (\num_of int i; h <= i < a.length; a[i] >= h); + @ auto; + @ }; + @*/ + + //@ assert (\num_of int i; h <= i < a.length; a[i] >= h + 1) == 0; + + return h; + } + + // the same, more efficiently + /*@ public normal_behaviour + @ requires (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ ensures (\forall int x; 0 <= x < \result; a[x] > x); + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result) >= \result; + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; + @ ensures \result == a.length || a[\result] <= \result; + @ assignable \strictly_nothing; + @*/ + static int compute_opt(int a[]) { + int lo = 0, hi = a.length; + + /*@ loop_invariant 0 <= lo <= hi <= a.length; + @ loop_invariant (\forall int x; 0 <= x < lo; a[x] >= lo); + @ loop_invariant (\forall int x; hi <= x < a.length; a[x] <= hi); + @ assignable \strictly_nothing; + @ decreases hi - lo + 1; + @*/ + while (lo < hi) { + int mid = lo + (hi - lo) / 2; + if (a[mid] <= mid) hi = mid; + else lo = mid + 1; + } + + lemma1(lo, a); + + //@ assert (\num_of int i; 0 <= i < lo; a[i] >= lo) == lo; + + /*@ assert (\num_of int i; 0 <= i < lo; a[i] >= lo + 1) <= lo \by { + @ oss; + @ rule "bsum_num_of_bounds" occ: "1"; + @ auto; + @ }; + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo) == + @ (\num_of int i; 0 <= i < lo; a[i] >= lo) + + @ (\num_of int i; lo <= i < a.length; a[i] >= lo); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo + 1) == + @ (\num_of int i; 0 <= i < lo; a[i] >= lo + 1) + + @ (\num_of int i; lo <= i < a.length; a[i] >= lo + 1); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo) >= lo \by { + @ oss; + @ rule "bsum_positive1" occ: "0" on: (\num_of int i; lo <= i < a.length; a[i] >= lo); + @ auto; + @ }; + @*/ + + //@ assert (\num_of int i; lo <= i < a.length; a[i] >= lo + 1) == 0; + + return lo; + } + + /*@ public normal_behaviour + @ requires (\forall int i; 0 <= i < lo; a[i] >= lo); + @ requires 0 <= lo <= a.length; + @ ensures (\num_of int i; 0 <= i < lo; a[i] >= lo) == lo; + @ assignable \strictly_nothing; + @*/ + static void lemma1(int lo, int[] a) { + /*@ loop_invariant (\num_of int i; 0 <= i < r; a[i] >= lo) == r; + @ loop_invariant 0 <= r <= lo; + @ decreases lo - r; + @ assignable \strictly_nothing; + @*/ + for(int r = 0; r < lo; r++) {} + } + + /*@ normal_behaviour + @ requires 0 <= i < a.length; + @ requires 0 <= h <= a.length; + @ requires (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ requires h == 0 || a[h-1] >= h; + @ requires h == a.length || a[h] <= h; + @ ensures \result == 0 || a[\result-1] >= \result; + @ ensures \result == a.length || a[\result] <= \result; + @ ensures 0 <= \result <= a.length; + @ ensures (\exists int p; 0 <= p < a.length; \old(a[p] == a[i]) && + @ a[p] == \old(a[p] + 1) && + @ (\forall int q; 0 <= q < a.length && q != p; a[q] == \old(a[q]))); + @ ensures (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ assignable a[*]; + @*/ + static int update(int a[], int h, int i) { + int x = a[i]; + int lo = 0, hi = i; + /*@ loop_invariant 0 <= lo <= hi < a.length; + @ loop_invariant (\forall int f; 0 <= f < lo; a[f] > x); + @ loop_invariant (\forall int g; hi <= g <= i; a[g] == x); + @ loop_invariant a[i] == a[hi]; + @ loop_invariant lo > 0 ==> a[lo-1] > a[i]; + @ assignable \strictly_nothing; + @ decreases hi - lo + 1; + @*/ + while (lo < hi) { + //@ ghost int diff = hi - lo; + + int mid; + //@ ensures \dl_mod(diff,2) == 0 ==> 2*mid == 2*lo + diff; + //@ ensures \dl_mod(diff,2) == 1 ==> 2*mid == 2*lo + diff - 1; + //@ signals (Throwable e) false; + //@ assignable \strictly_nothing; + { mid = lo + (hi-lo) / 2; } + + if (a[mid] == x) hi = mid; + else lo = mid + 1; + } + + a[lo]++; + + if (lo == h && a[lo] == h+1) { + return h+1; + } else { + return h; + } + } +} From f75f4e224cab810543551786e21ed2029138bc62 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Aug 2026 13:05:19 +0200 Subject: [PATCH 2/5] slight extension of the example and extension of the proof engine --- .../ilkd/key/macros/ApplyScriptsMacro.java | 9 ++++ .../java/de/uka/ilkd/key/pp/Notation.java | 2 +- .../de/uka/ilkd/key/scripts/AutoCommand.java | 48 +++++++++++++++---- .../proof/runallproofs/ProofCollections.java | 4 ++ .../verifyThis26_01_hIndex/src/HIndex.java | 14 +++--- 5 files changed, 60 insertions(+), 17 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index 9fd345eaf09..acf7939cd7c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.pp.Notation; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; @@ -243,6 +244,14 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ProofScriptEngine pse = new ProofScriptEngine(proof); pse.setInitiallySelectedGoal(goal); pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); + pse.getStateMap().getValueInjector().addConverter(Integer.class, ObtainAwareTerm.class, + oat -> { + String numberStr = Notation.NumLiteral.printNumberTerm(oat.term); + if (numberStr == null) + throw new ScriptException( + "Expected a number literal, but got: " + oat.term); + return Integer.parseInt(numberStr); + }); pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, oat -> oat.resolve(obtainMap, goal.proof().getServices())); // TODO: Perhaps have holes also in JML? diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java index d6f29fcf676..2fac70c0cfc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java @@ -620,7 +620,7 @@ public void print(JTerm t, LogicPrinter sp) { * The standard concrete syntax for the number literal indicator `Z'. This is only used in the * `Pretty&Untrue' syntax. */ - static final class NumLiteral extends Notation { + public static final class NumLiteral extends Notation { public NumLiteral() { super(120); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java index 1b276a3bbf7..505e0fc2d64 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java @@ -87,8 +87,12 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx OriginalValue ov = orgValues.get(entry.getKey()); if (ov != null) { ov.oldValue = activeStrategyProperties.getProperty(ov.settingName); - activeStrategyProperties.setProperty(ov.settingName, - "true".equals(entry.getValue()) ? ov.trueValue : ov.falseValue); + String key = entry.getValue().toString(); + String value = ov.stringMap.get(key); + if (value == null) { + throw new ScriptException("Invalid value for " + entry.getKey() + ": " + key); + } + activeStrategyProperties.setProperty(ov.settingName, value); } } @@ -132,9 +136,14 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx private Map prepareOriginalValues() { var res = new HashMap(); + // Deprecated: Will be removed soon res.put("modelSearch", new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_COMPLETION, NON_LIN_ARITH_DEF_OPS)); + res.put("arithmetic", + new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY, + Map.of("basic", NON_LIN_ARITH_NONE, "defOps", + NON_LIN_ARITH_DEF_OPS, "modelsearch", NON_LIN_ARITH_COMPLETION))); res.put("expandQueries", new OriginalValue(QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON, QUERYAXIOM_OFF)); res.put("classAxioms", @@ -210,9 +219,28 @@ public static class Parameters implements ValueInjector.VerifyableParameters { public @Nullable String breakpoint = null; @Flag(value = "modelsearch") - @Documentation("Enable model search. Better for some (types of) arithmetic problems. Sometimes a lot worse.") + @Deprecated + @Documentation("Deprecated. Use arithmetic=modelsearch instead.") public boolean modelSearch; + @Option(value = "arithmetic") + @Documentation(""" + Specify the arithmetic strategy to handle division and modulo operations: + - *`basic`*: Basic arithmetic support: + - Simplification of polynomial expressions + - Computation of Gröbner Bases for polynomials in the antecedent + - (Partial) Omega procedure for handling linear inequations" + "" + - *`defOps`*: Automatically expand defined symbols like: `/`, `%`, `jdiv`, `jmod` ..., `int_RANGE`, ... + In addition, inequations are multiplied with each other where the product is bounded by an existing + inequation (restricted such that termination is guaranteed). + - *`modelsearch`*: Support for non-linear inequations and model search. In addition, this performs + (a) multiplication of inequations with each other and (b) systematic case distinctions (cuts). + This method is guaranteed to find counterexamples for invalid goals that only contain polynomial + (in)equations. Such counterexamples turn up as trivially unprovable goals. It is also able to prove many + more valid goals involving (in)equations, but will in general not terminate on such goals. + """) + public @Nullable String arithmetic; + @Flag(value = "expandQueries") @Documentation("Automatically expand occurrences of query symbols using additional modalities on the sequent.") public boolean expandQueries; @@ -259,23 +287,23 @@ public void verifyParameters() throws IllegalArgumentException, InjectionExcepti private static final class OriginalValue { private final String settingName; - private final String trueValue; - private final String falseValue; + private final Map stringMap; private @Nullable String oldValue; private OriginalValue(String settingName, String trueValue, String falseValue) { - this.settingName = settingName; - this.trueValue = trueValue; + this(settingName, Map.of("true", trueValue, "false", falseValue)); + } - this.falseValue = falseValue; + private OriginalValue(String settingName, Map stringMap) { + this.settingName = settingName; + this.stringMap = stringMap; } @Override public String toString() { return "OriginalValue{" + "settingName='" + settingName + '\'' + - ", trueValue='" + trueValue + '\'' + - ", falseValue='" + falseValue + '\'' + + ", stringMap=" + stringMap + ", oldValue='" + oldValue + '\'' + '}'; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index fd1d85147d9..b81c52515b1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -415,6 +415,10 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("heap/verifyThis11_1_Maximum/project.key"); g.provable("heap/fm12_01_LRS/lcp.key"); g.provable("heap/SemanticSlicing/project.key"); + g.provable("heap/verifyThis26_01_hIndex/compute.key"); + g.provable("heap/verifyThis26_01_hIndex/compute_opt.key"); + g.provable("heap/verifyThis26_01_hIndex/lemma1.key"); + g.provable("heap/verifyThis26_01_hIndex/update.key"); g = c.group("funOfIF"); g.provable("heap/information_flow/ArrayList_contains.key"); diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java b/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java index 1b8de4330d1..e9297530e1b 100644 --- a/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java @@ -55,13 +55,13 @@ class HIndex { @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; @ ensures 0 <= \result <= a.length; @ ensures \result == a.length || a[\result] <= \result; - @ ensures \result == 0 || a[\result-1] > \result; + @ ensures \result == 0 || a[\result-1] >= \result; @ assignable \strictly_nothing; @*/ static int compute(int a[]) { int h = 0; /*@ loop_invariant 0 <= h <= a.length; - @ // loop_invariant (\forall int x; 0 <= x < h; a[x] > x); + @ loop_invariant h == 0 || a[h-1] >= h; @ loop_invariant (\forall int x; 0 <= x < h; a[x] >= h); @ loop_invariant (\num_of int i; 0 <= i < h; a[i] >= h) == h; @ assignable \strictly_nothing; @@ -74,7 +74,7 @@ static int compute(int a[]) { /*@ assert (\num_of int i; 0 <= i < h; a[i] >= h + 1) <= h \by { @ oss; - @ rule "bsum_num_of_bounds" occ: "1"; + @ rule "bsum_num_of_bounds" occ: 1; @ auto; @ }; @*/ @@ -91,7 +91,7 @@ static int compute(int a[]) { /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h) >= h \by { @ oss; - @ rule "bsum_positive1" occ: "0" on: (\num_of int i; h <= i < a.length; a[i] >= h); + @ rule "bsum_positive1" occ: 0 on: (\num_of int i; h <= i < a.length; a[i] >= h); @ auto; @ }; @*/ @@ -108,12 +108,14 @@ static int compute(int a[]) { @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result) >= \result; @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; @ ensures \result == a.length || a[\result] <= \result; + @ ensures \result == 0 || a[\result-1] >= \result; @ assignable \strictly_nothing; @*/ static int compute_opt(int a[]) { int lo = 0, hi = a.length; /*@ loop_invariant 0 <= lo <= hi <= a.length; + @ loop_invariant lo == 0 || a[lo-1] >= lo; @ loop_invariant (\forall int x; 0 <= x < lo; a[x] >= lo); @ loop_invariant (\forall int x; hi <= x < a.length; a[x] <= hi); @ assignable \strictly_nothing; @@ -131,7 +133,7 @@ static int compute_opt(int a[]) { /*@ assert (\num_of int i; 0 <= i < lo; a[i] >= lo + 1) <= lo \by { @ oss; - @ rule "bsum_num_of_bounds" occ: "1"; + @ rule "bsum_num_of_bounds" occ: 1; @ auto; @ }; @*/ @@ -148,7 +150,7 @@ static int compute_opt(int a[]) { /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo) >= lo \by { @ oss; - @ rule "bsum_positive1" occ: "0" on: (\num_of int i; lo <= i < a.length; a[i] >= lo); + @ rule "bsum_positive1" occ: 0 on: (\num_of int i; lo <= i < a.length; a[i] >= lo); @ auto; @ }; @*/ From 3f863ce622f23080df8363be96d6139edd72feed Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Aug 2026 13:10:24 +0200 Subject: [PATCH 3/5] adding h-index to the example index. --- key.ui/examples/heap/verifyThis26_01_hIndex/README.txt | 6 ++++-- key.ui/examples/index/samplesIndex.txt | 2 ++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt index ab45d06cac0..9834d42a340 100644 --- a/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt @@ -6,9 +6,11 @@ example.path = Benchmarks/VerifyThis2026 This is a KeY solution to challenge 1 of VerifyThis 2026. The h-Index is an (in)famous metrics in research. - -This challenge deals with efficient computation and updating. +This challenge deals with efficient computation and updates of h indices. See also challenge.pdf in the example directory. +The example uses the recently introduced JML proof scripts. +You hence need to run it using the "Script-aware" automation button + @author Mattias Ulbrich diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index 666003ded24..4a217f00039 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -98,6 +98,8 @@ heap/vacid0_01_SparseArray/README.txt ## WeideEtAl heap/WeideEtAl_01_AddAndMultiply/README.txt heap/WeideEtAl_02_BinarySearch/README.txt +## VerifyThis 2026 +heap/verifyThis26_01_hIndex/README.txt # Information Flow heap/information_flow/README-ArrayList.txt From 55bba7db19ed8fd6ca462a6a9adfa0bbd2b44ddb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Aug 2026 13:43:24 +0200 Subject: [PATCH 4/5] adding missing file update.key --- .../heap/verifyThis26_01_hIndex/update.key | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 key.ui/examples/heap/verifyThis26_01_hIndex/update.key diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/update.key b/key.ui/examples/heap/verifyThis26_01_hIndex/update.key new file mode 100644 index 00000000000..10384f1315b --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/update.key @@ -0,0 +1,85 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\proofObligation +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "HIndex[HIndex::update([I,int,int)].JML normal_behavior operation contract.0", + "name" : "HIndex[HIndex::update([I,int,int)].JML normal_behavior operation contract.0" +} From eee97c43390ddeaa664b0bbe8e1143bdb4b95341 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Aug 2026 16:46:53 +0200 Subject: [PATCH 5/5] Making scripts more flexible towards input. --- .../main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java | 2 ++ .../src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java | 2 +- .../de/uka/ilkd/key/proof/runallproofs/ProofCollections.java | 4 ++-- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index acf7939cd7c..ce2d352f6af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -260,6 +260,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices()))); pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, oat -> Boolean.parseBoolean(oat.term.toString())); + pse.getStateMap().getValueInjector().addConverter(String.class, ObtainAwareTerm.class, + oat -> oat.term.toString()); LOGGER.debug("---- Script"); LOGGER.debug(renderedProof.stream() .map(ScriptCommandAst::asCommandLine) diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java index 505e0fc2d64..ec5a402b429 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java @@ -87,7 +87,7 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx OriginalValue ov = orgValues.get(entry.getKey()); if (ov != null) { ov.oldValue = activeStrategyProperties.getProperty(ov.settingName); - String key = entry.getValue().toString(); + String key = state.getValueInjector().convert(entry.getValue(), String.class); String value = ov.stringMap.get(key); if (value == null) { throw new ScriptException("Invalid value for " + entry.getKey() + ": " + key); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index b81c52515b1..2b24ff31042 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -185,7 +185,7 @@ public static ProofCollection automaticJavaDL() throws IOException { * pervar g = c.group("- one subprocess is created for each group * perFile-one subprocess is created for each file */ - settings.setForkMode(ForkMode.PERGROUP); + settings.setForkMode(ForkMode.NOFORK); /* * Enable or disable proof reloading. @@ -240,7 +240,7 @@ public static ProofCollection automaticJavaDL() throws IOException { * test can be restricted to these groups (for debugging). */ // runOnlyOn = group1, group2 (the space after each comma is mandatory) - // settings.setRunOnlyOn("performance, performancePOConstruction"); + settings.setRunOnlyOn("example-algos"); settings.setKeySettings(GenerateUnitTestsUtil.loadFromFile("automaticJAVADL.properties"));