From 0266c00e54b8ac638d97e222accc3ff2b7d8bc23 Mon Sep 17 00:00:00 2001
From: Alex Chew <alex-chew@users.noreply.github.com>
Date: Fri, 15 Mar 2024 09:33:55 -0700
Subject: [PATCH] chore: update version number and doo files for 4.5.0 release
 (#5199)

---
 Source/DafnyPipeline/DafnyPipeline.csproj     |   4 ++--
 Source/DafnyRuntime/DafnyRuntime.csproj       |   2 +-
 .../DafnyRuntimeJava/build.gradle             |   2 +-
 .../binaries/DafnyStandardLibraries-cs.doo    | Bin 1358 -> 1360 bytes
 .../binaries/DafnyStandardLibraries-go.doo    | Bin 1378 -> 1379 bytes
 .../binaries/DafnyStandardLibraries-java.doo  | Bin 1339 -> 1341 bytes
 .../binaries/DafnyStandardLibraries-js.doo    | Bin 1885 -> 1886 bytes
 .../DafnyStandardLibraries-notarget.doo       | Bin 1332 -> 1334 bytes
 .../binaries/DafnyStandardLibraries-py.doo    | Bin 1349 -> 1350 bytes
 .../binaries/DafnyStandardLibraries.doo       | Bin 56992 -> 56993 bytes
 Source/Directory.Build.props                  |   4 ++--
 11 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj
index fc1b442d50c..473f5fda33a 100644
--- a/Source/DafnyPipeline/DafnyPipeline.csproj
+++ b/Source/DafnyPipeline/DafnyPipeline.csproj
@@ -89,7 +89,7 @@
       <LinkBase>DafnyRuntimeJava</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
-    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.4.0.jar">
+    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.5.0.jar">
       <LogicalName>DafnyRuntime.jar</LogicalName>
       <Link>DafnyRuntime.jar</Link>
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
@@ -128,4 +128,4 @@
     <EmbeddedResource Remove="..\DafnyRuntime\DafnyRuntimeRust\target\**"/>
   </ItemGroup>
 
-</Project>
\ No newline at end of file
+</Project>
diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj
index da6b9b385b5..d12ed975da9 100644
--- a/Source/DafnyRuntime/DafnyRuntime.csproj
+++ b/Source/DafnyRuntime/DafnyRuntime.csproj
@@ -26,7 +26,7 @@
     <Folder Include="DafnyRuntimeJava\build\libs" />
   </ItemGroup>
   <PropertyGroup>
-    <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.4.0.jar</DafnyRuntimeJar>
+    <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.5.0.jar</DafnyRuntimeJar>
   </PropertyGroup>
   <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
     
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle b/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle
index 6940c1f4a1d..638302fa736 100644
--- a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle
+++ b/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle
@@ -17,7 +17,7 @@ dependencies {
 }
 
 group = 'org.dafny'
-version = '4.4.0'
+version = '4.5.0'
 sourceCompatibility = '1.8'
 
 java {
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
index 372984519cc82ebae8ac43ae0d1002f74afca948..fd2be3e33cdbae862ee5880e1cc50bb4a0dac7ff 100644
GIT binary patch
delta 1216
zcmV;x1V8)E3eXA@P)h>@6aWAK2mqykZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEoeZ5$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mqykZdh~&cFw<%_#}TwD6~Z|ZSOm}0b0lSh`i*wT210$J5k5z|Bmf6
zi<9O@2LdKlOYOURo_p@>OOK8qB+KL;o_jC6WAAu$bOib%SNJ96?2eOoG#bS$%p!yb
zA2$+tvQ<w3i&LuBmLw9mg@p{glf{bg^n@ir#yKVuIHnN^P=K}eFaii7B7}bx?J|?(
zHo{AiPUg;Z>W<+?|C@p5dB#DxutZ3n1(NX^4YHvu-hy+tVnPB<avz+z@^|6i8Qd}!
zxg+CW?57+<8W4$aLn0bFuGuRP091T5kK4j0M!8~P8{8c4h2yIHWX2N#&RTu<L7<$>
zXYP>m|3oN%XYIq>3Xus6eVdaR0vvxIGig#7gOdDa(ELA?&5XGZA5uwKatP%sj9HFF
zh#}hr{f2gSfe#6hy4I$!&F*_6SxkesY%{t3$&R}&n{5nIefupfrv<cfvT*uqR2X)o
ze!+tE6H*=o)bWO`J|$6Mr&%dpyK6#U0kFGi%ynX48p@W&DdQ4YiV24BnUjAsMJ^t*
zGPyih%IAaw6?(ZmS);uycjW-UL}XmuRR5G7wInV|zWR^j*NoO}%MB6=b#qd&TTsc+
zCB@oW3Dk;XDN{rG6(F0X)daP!w`DW(H2S(lxW4vpvQKhHHigzqJ+%YVsWzy|(Aw*E
z>JQtdngxU%#BTm>I#xVOoX&rN)FD)T<n*i698ZVK(m!>2^;t4bq6pUTU43W*+7)~s
za6^R@kn3ly%UWIMbs2}JRWGnMRJqI!KpGxvhoqRR6my+o;cO+j?uI^SARdA)6}ql7
zm;fc9^p4fh@Sg2As69bj+O%NW0B)X?-m%(CntKZt<7-o&9US+JZgqdAwc*>K*<RNk
z%H7j>?>u(ThBNi*dH&%%(UXNlr)I(kb2`h4zP~=bdjIC)%ascF_Fkem<1E&0PD<oT
zl~!_^+*Pn;;l(NEjQhL$>{ff~5V{w>PHyv;voWByxD<C)kQUs}T(y7!zGi!{yTDb@
zAs+jX+m^R-t;{=;lM{dOPP8lZ_(nb`U={UmN!h~S&xu+!nJvnI0@fkaJg!h=k(^Z7
z7G{Q5F-VG66hq1qsA2~Gw7pW^KvCRRqbhTt%MwNZu1nyI&`4bXP6^`zsvmK%$O6?G
z!g(ZOqHL{_JW>C4JsfvPi6^Ar%4o;rmqc*fD*KK%&uXWYq~0yZjovpj)UWBBhU)0;
zRcySc>(~NO41NGmO928D0~7!N00;o3fNoeKqkr$alidU|AEkh9Sab(=&c6cy0HqHA
e00#g700000000000HlHDlP(1s2Fe5g00023{6f0`

delta 1215
zcmV;w1VH=H3eE}>P)h>@6aWAK2mq~dRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb<YNhgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080IhLVSbJavm%fqtB!3@JXp3OlU~~htj`0zB$#u1w#KCr=j?w=e+i4aj
z&5sTQOsbaJclSK^+}W2N9YIKz$vr&xo_ojM@#yFX^hd7nYs%RjC-G=BidmRN2oFAP
zB=Tgdo&px9RIM#ZBybB08G0v+72)X#OM;AZOeAnjBNCthYwckK5JW@>D}UN$CdqAt
zmn5Cco$1sa!;Sto1JCn}gK}YskUR?{<24#&Ls`59=WfM>1e)YNICJIi!v8b4Wh`<>
z#=qE4IfgVK65)nKG<00ES0DhW_-G!tg-?uf#lkkYIo=D$Rr$$`Cjy+c`tE~3IhoJg
zA?J5QD1T?|!`upy2@HLkag!VZ8-JfNX;K)2lKf`S{4L66#@vUGsiZ79gz^=}EXN|m
zknMtgM?1T~hlEI7Yg5=}_q~=ZrokJwnOy&3$6c4rHU_D_{gIZ_0$Mp)IQ=y$3_DW4
zV8QwcDGvhbc*9nolc=!MtQ4=^HKDHn*xfYdI<YSeWlQ6faS1HN1Vi}3Nq?Fm7mrz)
zTpldtbHafNy<DEG(O#CjasXf=GOli_|4NTq5*H<3{m1cJM(eia1__0_IjPt!sATAp
zVr{JiYQ?dXsUiIikj>I+f?C(xvKe_Aecd8lU;8)NC%Ge=LTjd;+JWg*8`NZI?R7i#
zhiy~M0>TbrH-9%BE1o4z=YK%z5UM_M`qgTVr^99GpE|wzEEy+J1Z()AJ~RRC3ce4x
zp+XAC^|RJxt*-OBjKkBa7g!srTxJI#4Ue@$Qp{C~xlXZgwvt?TLmxB{4?&j-UDp{*
zfD%x8$LeT!&-NSCo}evlS}<(@H&06MSnVavy#<T$m8s7Tj(bM8I)BsJ@NLj+uWJwG
z?&-XD9=m75nR@j+|9GD0$wH!2Ghu`|on=KoT%TTjczyBpN(Fp#FHxLv7Hc;rC32-o
zD>+T>D%i5{;*@j7{oQ?bt37oH-3#9)xA}|N7*JbWin}UE3+@-LTEGBbvpv{d;40`4
zkA28(%Uiit<~_;DiGO%6+7)_yBOes7iu$jlY+>;CM6H_47G*#I>kw)lS17VbPO5AR
zGsCMGB*iO=A!P|vF#~_vUMX*&DDKNql{wI5iK2hkC2&S)q%HubgmD4Yk2qLlfocum
zJQ6WcwpK}=sDHa2jyt5p6Vh*Gv}5vHA~<f9eaD+;wbM#c?=9m-?;9HG*K|%pb@cWs
zHr~^9Y=I~SKLJon0Rj{Q6aWAK2mq~dRajrfhn2dM-vlxrt#MUYdte2Zz5@UNr4IlA
d2LJ#70000000000q=Ds=Fa;V0$OHfY008&OE&Bif

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
index 1d848f6b15c93046376056e70b18d8decf689a4a..275aeec2dfeac8287011cb925121c5f398bd8a9f 100644
GIT binary patch
delta 1284
zcmV+f1^fEq3gZeBP)h>@6aWAK2mq>pZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEogs)$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mq>pZdfC4;XTp=008U{000L7003}uZ)b90ZN*pHZreBzefL+)_DKR<
zB@1kUg=)L#C20dEZIPtuV?axELRb=2k`kQt`rm&$q^yXNb#Yp>4PZnjXXczaGvvre
zM-Y-_@&NyMFT7*#cyx3G`lIgYZ7TSkAn|B4ig}nt6gGaq<CNjkl0=ejaUsm&_~9&0
zxlk80UQhwg-sz>=+h=1?B15Aq6?*UaTb=}&5HwLBXd01#O0d>8BY+?xQesTHR#YTg
zxX6DLSw!@Lq?5Tbow{SV(f?-Pd7g1V7oJE&2^1HW<Hjdz#^WtGclTT>U`g(SGe>_H
zp3h*xdE}0af3cqm8nS>W3O6KTq2rpp0s%}G=5bs2#8ln$unlfbAEe`Aekv1*1ZRcc
zeUMa5<}-K5`2&&Y@2q^7TOl$@L*HiH9RPp1XS9Z&o0WpW%`k&AMdO-3(+h=rq26$e
z&zUkQi~%LT88m-SRWoDZ!>3d+o*Y8?lEyrzMTjBWEA}6?vkQDkh|;w-g>81<YsF(0
zyy5G~^$&L3b=hoq67btEX*n&Rm6L_jU!%gXBlUA0te%kaAfS#nZ1p9H3OmgTdF_9$
z34H~??gG+RN$t`=TV^gF;3-XL2ww$BQ!3<RRwkE?rF>2VFsYZzlQr7Qa#s!jn#fGx
zP4!plQA^^y<g5P#{g$!1ZMi{0i5Du9y9G>!Eg7w?l|ZdHmNGS@p8>L2T1`;vdRsOl
zPou9}gzIbnCi^6JR8wfp)WaQ^PPKnQO@`K9w^QG2n`#yib`ZPyyXjc*EO9yqQio9W
zk<+hMb37d`OaIjA)n~~Ci6U6R|M+1EXjkxkplc?Tgj_#sT~>IV*JT`@R=vR55ObLw
zfHXYT4oNY`6my+o;cO+j>V`gOARdCQ5M9?9On?$ldB=D(yubGw)SjR%ZCZaYZ2&h<
zO7B?hB`v%w9@AH*K07$!8QtnkYs0rev%Ri8l)I<%-g)ev4X5~SdiLoo(UXNlCuYJ(
zb2`h4e!M=p{P_C(_7VfWc~DfI3La}WCnf40OREG+?kd=_@bW|mF8tknw$PqBgzklJ
zlSTgTYz$OeT*$jBNDJ;)fh~VvfUo%;>@IK>bcn}3<hJi+y&Aa(zqYq4`uGMvD0l_>
zr=)LT@cW8THKi@efCAQ`)jTe#%px_ZvMtOEuVU~NuQY~~B~Zl-{Aqioyn&*)FGp48
zz?LP7{&|?dDPa*_7)}Y}0>wsyt1Q6Qkj^6!6J=|a<ca#X>*2UVN<0W5{Z>XhCO;*U
zxC9~>d<RfV0Rj{Q6aWAK2mq>pZdf9tfA71K@dPqIs(@}-BX8k7(gOeh><<6{2LJ#7
u0000000000q=DuD003}uZ)b90ZBR=E1^@s600IC40B`^R0Nn%t0000^)k&BD

delta 1283
zcmV+e1^oKs3gQYAP)h>@6aWAK2mr8gRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb>v2hgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080I+dYSZ$PkjnV@E0PGI{00#g70B~||XL4a}#aB&l+c*%t`&Z2NBmu6H
z0zE8L+lzEJX#*#1kz~_jKudH&SQ1r|5}dmJ?;U?qRz%7Aa5mUBfDxITnfK<+kRu-*
zK}eR#BfRzAddJ@J=;#RaM?KKHRPcL2;?Zan^Dv7jZ2W-7DZ{5Fi6q_PLYT$z<9VEN
zp)P5>paNd~qnGaPUX4MC42`Z;=zZXS^CZZGpos!O(})CAg0;380R$0|5@XV}q9WPC
zWu||~BBGZhoy?u-)E&dE{x<{9^Na(!@I)d?pt!IcH$GW29&f?9f8bI9OL8BaIr_Ws
zdIk&5BX?x{i~Us4kOf3hxFrz_9oOs?2w<`>kK4j0rs{!*ZE$n?C><B`Q<+F4I4k__
zgQRLQpSeTMABjYNXXV4(3Xw?~`ZnY40LXtmqc!~8tP~7xhZ&qJ8rS@pUMSoP^@d}7
z$&^W93@G{Sp!o-?ni&fpKBtQD<PgeNH0C)iLJZknv+vZ-F7P2CO4r&Hw%L6ripMN?
z&)1Wi|JZRiWwYT)z;FLc%V`0voGhIF8Wn~esbBD5^^BAU0d>4#tACTIu+yxN*Y1Cs
z&{qKLE+BoC)GiIQW#;k$p3;Pd@KumBr9wVsWpdeA%I8D?lX|&4S);uycjW+}iOdAv
zRDYBnwInV|zWPtlZyBrGmK!9Lc%d@6Tfk)4lF`~)3Dk;XDN{pw36RawYJytV+p-yX
z8hza&TwnV)*(bT9nnG))9`3+&sttc?GPL%(o%&|mRI`AvgV@dAO~;C7iPJfdI)ti^
zoPM>M<LPi&`ln8>K1(i06u}C9;D;rkUBUN(u9;L4a{a7zS>bhFmvMMn^#W@{%w=`}
z((qV2B*h$4%yo)|vz6qk8~UJucnG>ebX{jK0ZKsS9plmP-t0H1JwaRAv|xYQ0B)X?
z-m%(CT6otyrhl3G?BIlFbgMJ14c`XM_PX{^?w-zj=dpV>oZ-9a`RDUQPZkoLnh7J#
z=`1Vy>E`t6)5*o%6$X6&sHi*>Jl1YbO4I|ERtc8eSFmN_<*5){_`CaTp*?j7-3#9)
zi~P^o7^t?ml=oGT7Tm7_Tflz+-|#)yUEnI{5RZMxZQsj!HF6JrZEsif=?#8R@Cx*I
zN#DZY*A<~^N?Vix1*}7>d0bJMMQT!ITbLPM#o#GkX$&b#po$sz)AmYv14VJ)jjGIn
zElU*r^Du!k!XmsdoD#+bij4->S%9q}ohKqD%GN5$GxcxR!*Pd{ct!{Mt&Da|UL=#b
z1R@vw1W-!>0u%!j000080I+dYSYO76mAaGi1TsIcaaCAtlzxrU0{{T*4*&oM00000
t000000001_f#m=I0B~||XL4a}P)h{{000000ssO4Z~y=R+ynps007H+VJrXu

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
index 87a2927d5a5482056286d7a93ebb369644e5e111..507725946bbd99336213c2bd86ab5c74fd9654c9 100644
GIT binary patch
delta 1254
zcmV<C1R49g3cU&wP)h>@6aWAK2mq#lZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEogs)$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mq#lZdk7p(R-`|005;A000L7003}uZ)b90ZN*nnZ`(Eye%G(K_DKd@
zB?C5~P;D3OkZh@wwn)<Sv0$W2LRcbIk`kPG{_lS!DaoR2IdoQRGhkRI@9w+%?v6(t
z9YIR&*dzQJ{T3ZZ$HCDNn6G-kZ-wCZg5*IE2rM#^Ai2#Da-Np@=Sro~@0=y25Xcm)
zf&hT#1s4i<fecglDo9bFka{D@h?H>7lZ6%p{kebOQb9!oP-&Jijp3H_EU>!?XHtnW
zQCxpOII>Fs$Yd!{!i!d;md#N;@YLGghzk5((!OlFK~kw>qq14h!O%O3y|or-5a$ca
z29bUS$n|m^Z0LHYcute|d^x$E^=Py70A*DS*YIk#kGNX6FE$3H|LuCus!(kcZ9I+i
z4os&;phv?WsKSxfSEXPQ!oE=x`f9z+W(|Mg8u?tR(C?08&mrfcRHhm)NHLj*)9Gjo
zH|A$AQQ=%mj1FU~FZ&!?=J+UGUKaX)3=-93KJ)N%#|6nUSis-<OBondh-1Jdl}bWo
zo((UHF;smT|0Gi5hKm^H4s<Eop7H=2K^@EN0Hhm|mDmfgvMY6nHwT7T=@2UuVy%Dd
z1i9D`eWoz)AyczZ1K0UF5M60>lV`97T0j*Y>(+>V*)32*tM(?=2t#FBd%6X@-6>nC
z5ixu!6y?lMnTW1<j&E&#8aNSI-uj+iV$Lh9fwtWo&g&B{U(vtNr8<d$k>P&Sip@M&
z#kf=`*xF8p52PZ_bZF*>gx<txd%1s8-P_es6g8dgHf^W4ipi4leEnn}J10XSFr^7m
zXlk0K&3V3RLe%!rKK6MTfP1>(J<9&Z^%(H?qsPEOUFET{-6S4yZ$EhSdzJ2y-CxMg
zBx&{F<!0c%T=$3XKdQc+nfou4-{2TNAYbj&9i+kBMKlBUwsv^rUfkw}=8=DL?pOA7
z*>m$er5T=mI%7tgWGB{&w4S!};^Xzn<;QpD-!AoW_5M+zJQX}QYGFatgD!C;D7)_t
zwYCA|i4a`GP3CTmrZHi9;``*bdOaHh8i@;e-x(Re{VH@XS>S8F1KSwxjQaf8g?#el
zl^^6VLz{!xOJHa9|Dtlhga3by)UL=}QalVeN1E~D5@ngGNf&J`X8o$0s(t~oPB{d1
zo<Tev&Q#<{%IHndMGo|?MKSMn3{DBn^z|ZaVMc(N)G?QdE)5xO9I;l`PD-B1|1cln
z$j8Jp!XNag@#LpS2uEG?d){liok1tfJ}%9^bwj^RS2WeFx0A8)4zC+y2Sj`D15ir=
z0u%!j000080H%O$SR$i;@4J)A1Tr6{fNof?6486C0{{S}4*&oM00000000000001_
Qf##DN1sVpo1ONa403d}{#Q*>R

delta 1252
zcmV<A1RMLk3cCsuP)h>@6aWAK2mr2eRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb>v2hgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080IqRWSfF*HBC7)c0HqHA00#g70B~||XL4a}#aB^p+c*q<_pjjX$pJFA
z2khbCB^kCuyLDN&q3ycILABXdh%I@NY^2NOzn_03+p(NDRk~q!0fIOZ$&dU<it^DB
zq~w-8z>DZbbQ~QAM@L}3>K?xpg5L>}2SFgP$Vh_ZCPT=1TI!!ml}3MamXtyuQ?LpG
z0GbzEDBuM$OyR2_MS()<jU*#d!Uvu#v>@ou-948IDk6YNvy5pBH=JjI-Ay=?N|cG>
z0>XchT>?NROMw#pXf<lt9MwHft?iAd!0#pP%eEUNl{z*mn*|*Vy`|V&Yk>xFzOZZ%
z=~sYUFW13_uGfm^G<n09ldD;eHcJmsR>g1y&u9CHtA+bwV^I3vuJ^18)i%+_(@5{Y
zbZP{8G`vL>j<mii1(Oi=jhfI`>uok`2-kne=Te1!cN}{TIp?J^)p$;d$vm7+M`O4)
zKYNJ^=UQTP7+ZbWr_eIT2kG*%(EnqQs3!B7ho4(6NS46@{?T8`z^FnT11_ml5-Rg-
zcv+00>eKj+NR1mVVwgM7rEGi318f9!EVBcUu1Qv6FTl#K)FECU7-FSEtW1ctvJ-#g
zVn6hm!n}t}%|Z=a=j%XprO{2E!5U}*RdlRdBl>f<Kn<<hn^+?Zm1*ti7VvhbY^6rT
z@TpLgGe2b_y5u>&viWJ?L}YpEdwPL6udoK%c5^tdkGOnEf1pcs5(6W{{iqe2d9aFc
zsZg-Boeb|uMV#r-%nu2@iP83Qr@DW)tD`7tI@@j9PH`2JCFS}0(LQ!ghC*OU6Qa=6
zG)<fHeAR@g?W29{^D+SUc*A>?{f+A};O|F|frGlrV`IBXJmTJd@aXp{-6Oldkex}=
z>cO+kz<svv58t1vzMYx-8_I8R3?GoMcIpn&VD2KC0ef3JJaR8?b3^k;Iro1nd%Eno
zd7jb?&pw?oqfN3CYeia5+j;Tv>g3|%>kr>9^l|m(L7_YqJU41#LDao2aV03b>khTH
z0py7gT*OW0Zj7ceVS3{G<fi&-HU=~j=kl&IGJyM4=w7nGS9}MyG29vT`LPT6=*cVJ
z%VCB#2eFsH&g%a~<$wqO9jSj^k-4OJ7;ug><HrTcGE<W-+FH!|RX0`r0%V<X2<kk8
zcsiV^$di=O%b<%K=xvK)-s>2g5}N7jMcBfO05hp$E)!iEGTb;~t*o7tJdyulKEjcY
zi6?|V=uzXzFOd+Ay6E@3*LFLDPMUpOntkhrew(gns#|X-W8)oO#|{~Y_TXPoO928D
z0~7!N00;oCaaCAf#)p-<lgtD%AFgp#SfF*HBC7)c0HqHA00#g700000000000HlHC
OlN|*b2DJnL0001vW>+}?

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
index e9759c618cdf039940d49daf018f044c261bbd29..6bb204b0e31b2367f12a6ab418499b55b1a96ebe 100644
GIT binary patch
delta 1746
zcmV;@1}*vB4&DwEP)h>@6aWAK2mq*nZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEogs)$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mq*nZdh`u#?j3M006}t000L7003}uZ)b90ZN*t_Z`(Ey{_bCK>xV$b
zTqOfGU{LG~ZI^Consi9A^g~f(ip(T}Wl<q1Et!9#|2~qUBvPhKIoV5qz?OKtd+y<p
zcSrB;!aTf5AK`od2Y=7s8}06b_-A+MDkJ!ogv-%rL{OH55elyp1WP>6`Nuh%`|ofX
z<%FP=!D=)Dh?f~A3~+{0G>6Y5%rZnMABd8WQuv6Y1s4SVcYB8^gCZmlQ}G(j1GvUG
z8OeXq2&a^hJYtxDH<qseP)c)xD11}TsAQLj-Ql^^-G~x&pU0+bJrK?*_bsOC1$QRC
ziIMTHHe|K)dzx4+y~L1?vK%#Zy<vD6M{n`N^y0vvP0|B#S_E(buMhf&tAtIl2{8V&
zjy^3s)+JgX_4x?QW<tQA;TOcbF`v(Jl2U*0Or^s0RoP{;GNCK^EoYt^j;2o|=Okw$
z8c)J(dhE?+;|W}fk6xm@V=gfs#+E6&4K2s$k?OoG_;UahvFY)FgP$8r!X$wOJn{cH
z1u+$Z0MJ8B8HGZ87rZPcP?$9S8d7f8TLf^dna*jwryPcbAot~9fThbY$&uk;A>V&g
zE?y3FvEVKi!o_N`=H#N^^btc#!*VQMREDed8fcwy>tdZjDyR)Ie~)hs|GV`76|{0R
z0k>ca(+X+FaCfJ4mWBlIDPu8C-INjk952yNa($FJ;!EC4q-SV}3sf2E!nCjJ2FT~}
zUr47q3Lp*b`?2iJ4e#Rw9ep}V86tmam>fQcPbzn3y`rZVhi9j6K3<)1g>N4jqVEY_
zifLXJvOB)CjKt|}Yqnl^dPoQ+fjZBw#Y~|>#KQgby7=*60!T=l(A!pt#qMXqLqHn7
zz-wle;#R2($GS<*jpAb!AnAW8nfVYF;XC?)+8I)GQg9O3YW=^cv>^B|NsWK-GUF!T
zCQK-5xjm0aoH4C7X(%=7l{%BOPW0v!-}hBs(Njh{aTSCQF<zD%vxt_LGJ@uD6fz`E
z)OfC{iIpOQ>qqjdxhpN^Hm4iMWOv$dC~#*3hk`+8x<g0zh<1oOPh-b?<D7NK_8+5K
z9n;P;%Drbr+*+0QFNB=6@Ed=yMs=NMbzL?F!(Db7RLy`xN-O0{%V7<#_<?fO9vQF7
zPS5kR?3;!(J})d*TN%+XEmHhvdaUhq+xVri6QzV~wp2C=U@5S0D+iWRct8=X2T^}%
ztcO@_8iJWH{^jd_9eeepKu$7VH@=F&Rk=QPsY=LpR7Eh(!uuSp1wSocJr>4%kvy}U
z5gPxfAx^5t#<>1m8MJ!lOQ6$PyF#$D)0I(xYbi}#>E5nulidUv3l?9;En@N4WvhHf
zlK}-6L2Aquh=-VlyAGL!3L=A#eT!GayQz(yS-Yx#!V#&MJF>pIHgAS^Y(v(mbwagn
znuFRJYT>`NdquOMJ6p!)-By!X1ss17<)&`XpjU#rv7G?y4y7Qpc*eFzyn=>PoFW@|
zM;qKdp?bRGO*de+nnX_+EmrYVG`Yjb5ADOZuv(OcOq(b4M=n=1a(yvb4sNu2h}hJB
zZ%YcVCJ-+)tSa|65C^YyN`|@Wx(2X#?cU$Y0n11v@IKXmpK3%exDpk^qUwLS#t-83
zzUV7;o^?CAeFY?82q)Rb(&r_0fIuqE*z)zpJKK%tjz&P!F$m1kRNsl=rgGch?-JMv
zj+gwr&=9D^g%x?NVDoO+Zw-TfTIjRgD6`og_#4E~pBx4vFuSDoici0ia@;>@$xoCZ
zXNcwro3?jNm6*(it7iAAD<OaFdaAt_5<so@WWM7{Or1Iv9+4`Ql`22J595T><ke<W
zemu{k2vO=aK%|yZyAa#*_RG$PH+C_xh5J@S3dxH|@W!q8J?(EhVg)J2(SsP5FfxLR
zc+O*UZN(;QyiPPD9KqjEO928D0~7!N00;o6fNoeKqkr$a0000w0RWTo1}q<_fNofF
osm9UG1polW8~^|Z00000000000001_f##Dv2O0+01^@s60JWewKmY&$

delta 1763
zcmV<91|0d`4&4qDP)h>@6aWAK2mr5fRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb>v2hgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080IzXXSSB4rfz1T~0L2^t00#g70B~||XL4a}#aZ7|<2Dd}&tI{<2gaG^
z44t`$j)8RUuF&3ba2=rB!_5sfjsQ;_%Sf^d4gP=ME6K7gIdbHX{$PelY^`>`{j}2V
zD!aQd3vbgWc;mnE_x!!l?k<Rbc8{(zg6~MU7>z~*Wl0#J@Fqd9z_XlxT(Ft{9;Z=G
z2uc|&M<alEkzv9BXDCH8_(H-gLxl2yC<!TrPdJ)$LEwLP_n0y$LIN=ruhA@k8;p~Y
z9F2c)N*T!`h6#9M`3eA~G$)9{clC@)c7fPEo=M$}C_xW-Y|7RH;f!+MVya$nXX4u!
z8SiRCRy)6^iPh3JhIEwWsG;jE!;3h2haV3vrv`139*EN-fJ=Bi?IW%dHpM2u_|q!-
zwD4G$Xo1w{BXD>q1PmH}LChQT`79?X1<!v}DqLTdT{bHdx{}{==DFc$`ZRJ*b0(tk
zG|Uc8yu-us1g^wKFHznJmlzLY%aq-OmJ{?ubzbKDIRJ{-!O7IY&n+fllE56E`G1^(
zm<mAv=rN{@LLt5jUgi@hOd5X;DYxs*131x4=d|8a4#Pr_`!XG1=_*WeWH?yJH<f>j
zR|8!vxQm5wv6`$oIqx_9fuV(AITkM}!_|5Xw9dG7vCbeB)CQTq$G3+6!)kyES~;44
zTd;*`g|uV1yHh$#Ljw4mu^6Xr%7}k~7w9LsKFS>NC2uCubF{z(stk2u+Shdr<cs((
zq*EOQkcRgCSoY?I<2XSdK7U9VB58k^96gFpDtBkSqGy*!=Vxy}U7vG>@17W<#{@6L
zG%pL;JzrWz;`FXHTQ594A_S8_oo6><rcfbb;o;z>_;ES`BqUDhU8}@m_Y2`6APryQ
z6|+iltJH;K)g<Re@v#h$^uLtMd<={5J^e`S3@JJ(I0<aE{$EsD5d4><MtFabaT9PG
zCKR>YUPL6$m{yxKlp6I)ok?0JdUJ~J`zo*KDWjdZ48q44FUqx9M9WJVL9;jt84@RI
zJX6)gQjx*+Bl*?bl@@dB(~V=YJ8d`=xU+#n!JsqUp`&|5JH(x*v17h*&N^iKk5R3T
zY3CW`-isn`rONvkLe5(F4OoApy3Vt@E*pd4E;|jXX22n(mGY(Ku!dLsK)G&@j8|o+
z=lNOoO+y-=EsNDwMl?+G6#to?Xgl3Der4=LDIuFJl}!Rz2rS&n)KUr$D1!AM>MxD;
z5UWi?a43v_{kC7nUOg$0lZ@AmuVQdnu8v))60#jt5sb6&AxA60&sQvug)v_w&n#zz
z#y@I^lj^ZCu0K}>t)BT3=)qyTLa?*bl~I6eDNSAJ-mWW?-UJzA=ikOHV)55yt9(JT
zql!>_!05Q!uBY3K$Yw!b?wy@ZA-inM6^MtJhPw`#xe6kKk9~_*!@H@qo>{x9f5H)|
zm^-q%x;AfycWgt}sdYlNZkmJI8fxLcv3o_cp*vf~=G{h<S_K?`7UjBb(4bd>y0x7E
z>>i~cw0Oq0N4$cDGn^tDct;!DJ)wHK<8?P+wwgpw7%f)uR5ZE6$Pewq_pqFohD@6$
z^hYjNG;)10Sq^Trdx%)qe{V_(uO<*LG^{H3*ANG<bxMZ0>beH7c<tWb$^pwrB=A1h
zfS+qbTU?2XVNvye+~7xXdSCXHIxo5%-Mj*lFoctAZRxX39UzcOGq!xa_Re<gxuX%#
zbPNKsG}U)vxT)MU_`3vlf@7PX7a9VUxUeFx6>Q!O`>kQnPYZpv8)Y{81Al`U`jf*z
z1ZJ1iUh(NyQjYs4E%}KO<Q&mFVF&G9Qza&|;j-Di>Pkp|yPj(Ag#=LRJ(=&g5>uy6
zg-4`HWu?lG$6=gsn!MVK%8wU$6d_8z28h&BY8PS~-hSEn@Ww7CHgMmHNFmvZ1aI7W
z-_!oKBUX@N96gG02_qx8h-W-DS5|DY!s|pc!V&xpP)h*<6ay3h000O8uW?maU&e=(
zx&QzGIspKa^9C#*uW?maCLKh9%>@7e#T)<t2LJ#70000000000q=Ds=J_i~G*9HIp
F006GeI4=MI

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
index 7f4ccd56801ee8b39c808999f1e12774f372abd8..338a7f277938e7f5e725e2dfa9c594730358016c 100644
GIT binary patch
delta 1268
zcmV<Q1PlAL3bqOpP)h>@6aWAK2mqsiZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEogs)$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mqsiZde$=|97PW002-9000L7003}uZ)b90ZM9czZ`(Ey{_bCK`z8UN
zk^w7FsJ4f;NVdR9JH%P~v0$WgOjsgSk`kPz{_lSyDJ!C6y*Mitz=%xV-SgaYN1k<d
z1~FN)C-^;h6PyR<le050AGN`+nc$Ctq?5@c<#C=MJcqbbDA-;<MLf-@UR#qy;vQBi
z4nD3nL}VX1i*g~5DG-<?Bti+!+Vcb;N{EzBw3}R!hXij(Hd}i0xj%(_^KSt`5LgH8
z!kK?mB99ao4H{%edAbMhal@qo%8C%YrS|vX*9AOqp7;~%U+!lDV;T{Ka8D8%d%oQ(
z5dd_2w2%AJCq=d4aTnYYpQPvO{8TQO1aGUqhageSmJ5H(`7a{1zqbux>4eB7#-Yo&
zKY-?*V*|giD<y;baRyfk(}q7a3#EIh-gtkEzjI|%n1Yu4e$@O=RPBsK2%j@WIXi{&
zEvCG{GQ^neihf5oyC?)kl&Q5XY`gp3E1uHm1K-W={$t18Rn0a9rN8|zEoTIDa&mBn
zYg8Kcq<+n#?JH6q1vK%-t^Q$2X=hkzUWaSKTmf*nY3z04UK-k#rWqFsc!msP_#%Hu
zmZ6X@S=n5k9pwumfJ(Dmovg`GmWOfxAd|V!H`OndM<a>rim&+-_${YR+iHWvQs10Z
z9u{;mbWO3bRsnV5ILb7Teg?>8=`=y3>s{HbJgvU&5N@db+w584skYFDX`pvtJ~svp
z89IC2P5pV_R<nd~gSgG#PsfSph|_;Nka~n_j+|k&+T-bTS%#<1pgwCZNRq%7e&`Qn
zU|b;#0e4g?359t!x@`4z-js2CS`7jlL!Haw1f=n?c1ntcPO&g4md;L++kWVi2I48`
zN~4=PgAGsts^DB7jo`QA26ZQBN1K*RTfps;GB{QTNsC~`Q~bl$=Kv=Ht6P7QX=C`d
zXm;0ifO7wIK01&6v*A+z^t}3f#mr<O$%UOT(w@$$qMz<AZa=-h{(7qeet1$SF9lDH
zo0k!_(WO;_vd0>>D!jZ9f{XBQpFJ2)6T<Yux7kDSb}<Ds7B}*-4$^`9Md%i=z<2xz
z_7J!ZI>zG|a{uzHyw<}NU?hKUr(X<@Ta<aCW_6CGndMd9dF3><q#RjlW)RMyvns(z
zDg1YnI&+}w3dOvFFt{W%(Y@+bFg~Du-+)yf>Gulhy%4cc_D&&QseiW~o<F9<E7I>|
zbYSvRB6xnCeb0}idZ&}5*~gvPw>0#NUqNGixQ{9}J<@gRfM^E)0#Fo70Rj{Q6aWAK
z2mqsiZdf9tfA71K!vr!vqkwK$7{LE`r2_x}P!0e92LJ#70000000000q=DuD003}u
eZ)b90ZBR=E1^@s600IC40B`^R0I&oA0002&R7+(5

delta 1249
zcmV<71Rndg3bYCnP)h>@6aWAK2mq~dRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb>v2hgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080IhLVSQ2;b9HavP08kD900#g70B~||XL4a}wO37V+c*%t`&Z1~B*3d=
zfgTFg_M$D4-M~p(#M$&%Fw!_CERiZn2~Jc0_a%QRE23n5I9qH0BQiNN@6DSb$2vQM
zn5@|oyb0a}=fU~p><r9DZSY$r_@f}{WHL#4oF@p+A?_3kw%1P)Pcy35)+CX*hn0$h
zkE;z4*+<TzTnJ<e1ZD||P=d4eJOPLjBBc}UCRgMk!5fmzmfn2sPvPGDTR;#5)<L^)
zCY684BgI972H8=b?!kN9aH)W@A_Q-#{eAd-0S}xf{>1v1`<cL)MnoaplZ3{eZ}&<B
z039Fg<G%DsQEhnK1-HZ}>G?W8l?x`p+v@KjNK~`s!XI<~n@H{NZ9`Z(A##av=rZmP
zpt<MRz%T4d$>4sR!Ii?a;ZMy%>0YWg9^-#Yu51cZ(30Pen*W8Wov{evbEYU~r%=Ad
zlowcr7_(i`ALwQmg}{h1wYG(Aci(%(QyP8XyV>1;?6|wC*`}cMxBsQ(jDSu~4$g3m
zO2eMiuX(h6MarXqCf>N!KP)Nj3@gp+a7~yi01h{ey-wUqL)+3c<3a(?kYNm81<8Lh
z6!Il2o6EDKd_e?IX_l*#H95-iP!0fOG8g)$`mOS4BynBwHGcxX=d@{CZID>%o0H1J
zf=-66DK^$BpiUe|nFi9Y0J$ukCTMiME1Q+4)z=-u4YhxpJu5ub7TPck^bXAD#-JfX
zXRo`dKkwUWmJn_bxB2_&IPn~DdIx_}k5J8#Gpts7Je@Af@YEU9XUzpk64=5|{h<tu
zD}*87j!Gq=FwaJpt-j8iGLBEHL11I3b6K2#G(Of&NwLr=7AD2g*-3KS4}H==JOy28
zbW>-r0V+Thoa>_z{Bhi%?gZ^<(~@ZmxP4Lv$Lb(y5v+KMf7<#S;6z|`YchXr4Br;b
z?z#?8?w`&_=dph_T<V{mSD&w#nJgr^uoFhw(^*yY)7{1Gr}x+2Zgs#9PYUIw;Hh!*
zGNLxRv`SF+Si@F@mlr~C5gzWd2jgi%m|plkdnn#6rhvxcMn2X-I&i-V-2xW)jvv7u
z0@p#ucpO9SUw)O>dbk3N<n4d-i{WvLGEda3&apJJyvjSToTiqPBTLN;!Z~zSB^W7%
z|87!e4s>0im{$-6mxLy|SG@|x2h{Hyu*xI-ULm~~A~wq2Da0%F@7BZf$CP+Q`kjmp
zOnylO&#$xZ`H@ubbdogtxHJ2fhJNuYXsi$SQN^Z5x=tMs&EQ{9O92uB6ay3h000O8
zt#MUYU&e=(x|78OG6}75Rag>t?Hr_%1r;IX0001Ra&KpHVQo-L1qJ{B000620swFT
L006E800000%E(Yw

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
index 48b62f1901553a2bcfbdf321e4623a845d600c92..5b3c4f75d729ebde53126af9c2091a986189521b 100644
GIT binary patch
delta 1267
zcmV<P1PuGd3dRZ(P)h>@6aWAK2mq^qZdf9tfA71I6DNOZm%T`f!XP9nAu5ppDd%(h
z$_V1N+ZnvUOR96`Li2^pS!MUW8>VqTgoIh{f9dP^HttvBS~{LNku=Usw%U)wCjM=v
zmvI`xr=D9!{uM-_d(QW+GZv??2uDo>@q}xs*+PLNt3`rDjjXb;*QYWnc<Ul}+6d5{
zk5c=UEogs)$srb8oE%i3Qafq#X8}vmE8vZ_`ZjvNE1Iwze{nO6-*7gT29z_!wq<?*
zP)h>@6aWAK2mq^qZdj<^L+rH!0062F000L7003}uZ)b90ZN*n@Z`(Ey{_bCK`z8aP
zk^&ttsJ4f8NVdRDTO?Wfv0$WgLRcbIk`kPz{_lS~>cygLIdoQRGhkRIkM}(H@OVd^
zoIt{s;t^hlzl5jZ>FDGH?AJWtmt4tv#j??8q%coejO;E&$YfH`&$UUy-=&BPrBE1n
z8jS#WmP=(o<|r_M&x++aDoqn{%Cv^}GG37((C7X^Y6B%xz_lI5B!W9B(@`}WOQDS_
zVk3VQ1mkK50EI3TYWS&LQQKx{9%NGa-kK`>TJXMYJHZl7v2ooDP%wPSu{YKN4dVPI
z(m|vj0diSxMq9bw8kzC<om@|E<~`Xed4P*Df*bgGen`05xNkNAL;v>Ki!v~~LR+RG
z&A@DC4SF*CfhHK!dQ&K&A?Q1`p+9YQ)vSLZTqmCj6Zq*k{v2^G3uCkKlI7DyFq@4h
zaBF`K3KcBKVtkxhecPAFvcN~}>awE$5ok2i#oVLMQYx0Fu!8UO<pS(dh$6r>*G5BW
zpRF#d36y;q|74nQgH;3z2fEPhneqTzLyBd71kx=_3+x40RwH$Yw?~FpQi!Duv0i`d
z1i3m4ePJ-`A#*!W1K0a?B)TDVyU$QLXaP-lN=GAnwV$9?R$>zo!cdylOm~2HPs+~L
zs0cphhD+g>Ooi7n!{4g?Y2Z{?>DFg@g_$g|2HK@LysyttzUJT1l{$_<u;KGa3!8rM
z6ye&S5*vDoWtMXqTe4K+rfL<R9?5^TIH%Ezj~Bukvh=K4Kta~sMZ@s4J<$!b4&>s)
z&Dqt5x9`7P5uJCB2KBj;nRO84%sfzH7{$eXN4iZLeWsLDQBw`?>`LpxX42Q`UHR*L
z0%$ER^?m2$Sq7gKrBX%VM(z=4AUgLxM*HBKgZ<a5*Z-x`f2qwj{|;uIb4`EQrdsdn
z(l(WDa}TzcFbta(<8}`>`PrJwZ1ZeGaavTaFyS#XXp1XPnv2C#BLw-!>al-72jHIX
zJf6k=4&rg(Zwwv>N0oPvkKJnRG4~c`&-z};_1GS+sLqw9Ti3h!{iBTAyYT%BDK~fr
zJYtX9E8k$~)jPuRA$tLv_X2;9m2<0ids<gx-J<HLrA|8818{}9NX@jXo3&Y0>*^Tm
zx1g%fIi<F%b`Z^mJ7ef6@8dV4u9^a0wkY=HPQW?iDcv!G7G?}cbrY_OnChbrwnQo~
z8>hIxu%-{|5sZCGydeBRMh%l65+N9O(I0rZ?Pdl^+Id{t`HBX;QkNt=q5iYCW0O5y
zCk_ZP_#0450Rj{Q6aWAK2mq^qZdf9tfA71K)C4jJtAK7;sNO^DlMV$IA?5%80B~||
dXL4a}P)h{{000000ssO4Z~y=RzytsQ004SJTNwZV

delta 1266
zcmV<O1P%Mf3dIT&P)h>@6aWAK2mrBhRajrfhn2dK6DNPoHWz787=%P6L?tpH<$P{m
z8AaS?JA*fPNp;R#Xugs;tL%=uVH)>CNSNjEpB~1;xL=KH>3HTu(l|5OYCqmL@v@oT
z#%TzjdTAZ`R}h8nIX}A2Se(Kl95oTdGp?m(3k8y_76}qHvdY3<pUSA<y^GvwBS3dP
zN$pp*pb>v2hgfiNa!`Rv?X1b41uR8xfOppF+vpeG(1hjmhnr#ihKsQ@pqweTE%O6V
zO9KQH000080I_jZSl6~J^|b>40IClF00#g70B~||XL4a}#aG{N+cpq>_g`^)lL1f3
zfIbYG?V%l#HgMAxNtQkqjC4*2OQcFtg45LhdyjwmVNtdmIxDsrFf5bD`@Z{lyrWJ|
zAYn`K2(Q9d;c0j}IynLRH4peDSMpx5Y&04v%u^O4yGs!=nH2PMZIbXWDdIvY6b7C~
zBLJS|QW=mr3QXX$VtI~A(?pyyt>L|lS7ZqExqpz_K*<zvZHF<5;7-bPRL#axXrqeQ
zNCkhvxEcaLp$ml?erZ?Kwi%iSnN+^FrV76nyl>l1utZaATsH$03}15WjkQ37IDd<D
z5b0-tT$Y>BR<74ZW;}i)*VCJMPqs=P;G&G+27a9%60SDxn@zybzkT+i49u?3mT5>c
zFq>I}o(yl%1Y=rn3MDiIeWy0`r_HXKHH3fb<Wpe+KOM)PBhF=EY&Kr9e7Xo`v+)FO
z?ax7>f(2QOk5j8}`x03e_^4f7R`fptjb^%-d-PdK#nKd3@SVO~fL#hv1i0qfXejNo
z)nzq-vM=L1rU^G#MX+$73*DY653n_)Sms9{-Lka6UVvpaQiphZWQZk&SlSTl#ZG^a
ztHaP22D2VAw*xhBy<bP78$!4H43&cx(1fRSG{WEZ6V%E|Y$8G!O4FL@4)E?t+1VNu
z!N=TiDg2VD@LFd0XSF{KoC+)5`b@7dlO@(byEKRQ^%=_7{2RJb#}NoNd>(0G(+{2^
zTpLtkLr<~Ha!zAQmTKHot>V)oxfXxtG<xyzLRdqVo>dDd$hx~|7@oE#x?$FVTzt4W
zyZZ3@{g*4E^XAc@K36ic4uYJS2TBa1xVY~~w`rr#l#(iHs^OhoX<gV%`Z~QUf1ghP
zt;MCj@0>i#;IpDsswmvZJpv6x=ibL?AAEDL|9bWMzf}4!wb|z1!K`zxDcgTk>s?*i
zrqXTh!S)h{VbfyV?%^gsTXUIho^2>ji^>%yJZ1)Mapg&Kv3P2PApclB_7CU)-1D8s
zv)JE3JP!Pg!Q<el^6v4mTdh6j-oorz-z&Ku+rt&rxzcp&dN;p+lyQ3(zJDR*2Je7J
z>`{B=8w|aAM>sxYFJSXt;IV&lZuM?Y>uRi9R6VuSNhf;%u22`LnRa!vHmhn~9b^3#
zR24d>)OOVlqS<g~3_az2{Ku%Profjiiha2gaL#y2cZ{Hg83R(?gzF-v`ly2~k;==)
zDef<<>BD*iW1kW)2!D`K!{nz#2*zFX2VQQwnL(0v9@lohqCv0JB~K%$|LpD9WKY+L
z140ab08mQ-0u%!j000080I_jZSYO76mAaGF1TqM*aaCB?wk-9N4+Rz><p2NxaB^>F
ca$#*yO9ci10000200IDT0002L1ONa4015(A5&!@I

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
index b6bd99cc7041ed44027551574cc04aa449851d8b..9e0bfd281d9b5aae6c6b824391215b98a3496194 100644
GIT binary patch
delta 288
zcmZ3mmwDk{X5j#DW)=|!1_lm>g$;QTN{j2?@17{EUY|LAuSfSG1r;qtt%;19&x?Pb
z;&`;}w&b3J-m8kAIel(D6PfybpY*aq`<9l-cl9q{|1f(O{y55Np5;W7b3WT{^&eLI
zm%D6wq12(}^P=7ViMlMTKKFf{vDoqr9PYj>A6v3l-gIhIS?${7(z|BUhU?3Xv?^XJ
zmEYpHFt<PG_f*{s`<9c6Vli`MLKXyBXMRd&^uDP5pm*ypv#JByvo^@o7aI56FEE?N
zHpTepw$wTXR6lh7&U-%bdj{j-%?XUh?r_4rHCg|jkvxb8QXp`bfkCH+m4O}Tbr@LE
P_-t~+Jt;Qndms@2W=MS!

delta 287
zcmZ3umwCZnX5j#DW)=|!1_lm>HHD!O@yFVy?wTm9UVqk1JTp+D#YNRc)kxuKO<ugD
z>zy>~X7dWq(sMBx`zBege$%%*QR=(1$Bd^R=gS>Cyd%Ch`(?#5mrEALH?!>TnSb0g
z^WL#cj`>xYvOmKGTHjgP?>ZMT=a7<&so)XgbxYH@StqR#;}kO8bm~yt{8K9)?Crjj
zsq9d0=lM2#+X6v5wf2aD!lHmiueWPX&S%we&2K2b_UiTv@p~6qo_=Yco%pA%d!xyM
zIhxyaKQp6xK~=kP`@|m^jLn-98IRrJg!^i;!962+5D%n4;4TA$P7NyqJJ9Dau%z+n
N<i>kaY*P0?A^;uvcewxn

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index e8871b3b2c4..c2b53231ed1 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -1,8 +1,8 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>4.4.0</VersionPrefix>
+    <VersionPrefix>4.5.0</VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
  
-</Project>
\ No newline at end of file
+</Project>