From 769d1572fdd799c7bf76b78a3bc9cb94d18aac59 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 26 Jun 2024 13:40:01 -0700
Subject: [PATCH] Bump some versions to fix tests

---
 .../binaries/DafnyStandardLibraries-cs.doo    | Bin 1522 -> 1523 bytes
 .../binaries/DafnyStandardLibraries-go.doo    | Bin 1544 -> 1545 bytes
 .../binaries/DafnyStandardLibraries-java.doo  | Bin 1503 -> 1504 bytes
 .../binaries/DafnyStandardLibraries-js.doo    | Bin 2051 -> 2052 bytes
 .../DafnyStandardLibraries-notarget.doo       | Bin 1498 -> 1499 bytes
 .../binaries/DafnyStandardLibraries-py.doo    | Bin 1514 -> 1515 bytes
 .../binaries/DafnyStandardLibraries.doo       | Bin 57166 -> 57166 bytes
 .../translation-records/DuplicateModules.dtr  |   2 +-
 .../InvalidFormat.dfy.expect                  |   2 +-
 .../LitTest/gomodule/multimodule/test-go.dtr  |   2 +-
 .../LitTest/gomodule/multimodule/test.doo     | Bin 520 -> 624 bytes
 .../multimodule/PythonModule1-py.dtr          |   2 +-
 .../multimodule/PythonModule1.doo             | Bin 661 -> 765 bytes
 .../nestedmodule/SomeNestedModule.doo         | Bin 665 -> 769 bytes
 .../SomeNestedModule/SomeNestedModule-py.dtr  |   2 +-
 15 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
index 7cc6a30ef0e3eef87e1c7958ae106da16571dcfb..31b0d8dcd2d15f8569692b4a4b364be7182575cd 100644
GIT binary patch
delta 494
zcmeyw{h3=hz?+#xgn@y9gF!doRz!Gh#l?b&!s_)Nb1Jy~6ij9w$<!5EZozr`o?Llq
zs&mZ$`y1=)`_5O2TU>hAy`^B<?B%oTcJF*^-S5~p{ng=Tg~is^s_v7^-*{@VtIfST
z{rA-!Rh#$T&iVb$)c@*|PuD!zK3mG1<&)qp^}Uhm|G;gIb!hIDi7jjT4g{<E>cm{S
z8Pru_pgbdrvwnk!oJ!=Bt%}EHd~aYsxAKqR_Z5eX{!F#?_2PRysjBc<kcRTFJ=?`s
z$7prAe--!{8#uGBT6IdB;Hpms5>281bAB*$oeI>F^Go?vT)Sk7KtxS(IHQetO+U*d
z)lC9gH+ER5t$MRASj~*XsKNNqu@hI<7%Y^UJn@w4f#8jzp|0oai?0?QyMC!?w(*1D
zsgv@zEx+<#i^pzTgrbS1Yn#o&$5!*V)Q3&k#IxN#Wpmv*TVu72`j7P{u9aPPKx3i)
z10^$W{%5z&C4YNebNanqLeRE%B1}7XMV+>NnQ-5&=k2C9kMxE2Gopt4<(r-p*D^CO
z9OY+VU}xC8jqwmOCp<<bH?kVpgLtT_fYAm8OB!c0GB6Yr<);@V<_37PvVp{zfUp2a
I=dyx$06F5%zyJUM

delta 494
zcmey&{fS#Rz?+#xgn@y9gW+q(iU|Jxbqn(+3ai(5Nar8qY*CwRvDWpGh<f7f+mF|+
z$?16g-}>A8^B*nWGr8ZYohWv$=yS>CeDm$K&kav}4640hlb4si{7J^AK3mVH2bOI9
zU9?{+JbzpH?A-f%pRJq~a?k2yf?fOKn~cc|*KzKC!+EEpc=@Vct4R~C3RbLI(%I^5
z740R+pT-ib%~(I}P_s(+CbJ_FpXELru$*fDNG>#@ZU3g_o+lGygY?hEaHYD;|Nbp$
zs<-RM6>>`ZwY4tiuWz|z;1nvy=Dgw6eBOEoM@z4xhdX`h*Y!^kV(QL+r`7Ph>HS29
zO)g?itkU7fU8deGJ#~c5k*&b(hQ!WUqG}<@MnO9{DzvsOTJ@r`ex231A5l?x#cVaJ
zf<B%7Hsx1*>%rq<+AV6!PfSoRiFrQx+xf1bX%D}(=Uh9#GyRy#x70hTo3<Vnl~Db{
z8gnG=<-wTSm1pYa=Ks9Q?sMweTqlL_@a&!HvTts8Y>b^2`zQ60IcmUPzUet}Ei(hd
zQGNynb_RycI~Wf#bHZa}auchOJ&1><3>a?^u%vMoBLhQ0QGR++Vs3ypD;r3d2?z^-
JbPg+s2LQi9*-rof

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
index d2f60a68e19a9651f1cb6a42cee16a8d237a08d6..1aa9bd1c42bf4a9e0b3ceeb73334e8f7ef0fe1ce 100644
GIT binary patch
delta 472
zcmeC+>Esa(@MdNaVPIh3V6Y6h6%k%raj{^cuzJ16oC<C~1(TUaGIfQPTX5dKCs&@D
z>Kya`{>J+HzVnsh7MI?2Zz-5Id-?3T-8<h}_dE7Ye|7j-VX?Kfs{7>fH=bJTYIE;S
z|9y2w)#kmobAG=w^}o90(=|`F&z3T0`6ReYeQ%`tKX9949h!S(V#}Jo1Hr1kIx&}S
z26a^!D9?!EtluCarxH13tKzX4-y7J^t^6bSeZ?W8KT~aez4%^Fsw#XIq@nz4&vx<E
zF<M>jUj=@~2F|RjR-Mu&xayOEL{sShoFB|wrvkO){8D}u*DjeN5K&Vc&S)cE)6X(V
zb(4VBjU85MtKO^&Rx{%;YA`-@?8MbI1`DMoPdw#%Ab6u_sO$Oq;;V(nu3sveZTuj3
z>ZJT_%dh;`;<4Knp=e_1+GexxvDN%7^<h&s@ocwG*<5$d)>v(${$ss~Yh~9R&{(Md
zK*`LT|Jki`$=_broPKYY5VY-`2-D78QKxNRCfs-HdAsS&BYolhjHn@h!suG(VP*yf
z9svdhc81N{7;i9h!eeCebXFr~AaC*+R%ylAj0_9~MfvGPiMavZtZcxzV_*Wp0wCSY
H3gQ6($v4Vp

delta 472
zcmeC=>EIC#@MdNaVPIh3VEEm!B7(nv-NO8d!s_)M()kBDThu07taW`PqMmsB_TzPH
zaynlBxBmA2{71|8OzyX8CyJdb`do53-+X)RbHfuKgKBTs<mII=f0FU3&(`zlfhC)N
z7wwk{&)-%)JNN$HXDerg+_O5FVAsC*CS&r#b)383aNg-CUcRc=YSM(Of)%Tlbhdh1
zMSBVIr?CWUGuBT#)U49I$?S;4XSojtET`H(k_(M!+rMeK=gGv_ApLVOT&XVezkf@b
z>h1b*g`CoUZLQ1s>su}vIEBiwId6D1pSRw@(bDVa;ZC3Wb^TL>n7Z@dX*E1=dOy)&
zlZ%)Wt91Brm#KG4PaR=%WGisHA+d9os9H#}QP56~3axF6R=udKUuSjhM^sc^F<Z^5
zpigJNP5BkydhocIc8l8b6BE=+VxCX_cD^fU+QV<{IoHnbOh2abE%lD-rmcrXB~-t#
z#vDm|c`)X7<(ay<`9JTn`<%Kq*GVBfJbS0Q?3>#i8)K)%{z-jgjvDYMjIMPaW@cdE
z5ny0oXJFX8gYh~uCp<<b&tNrT2J$AKWtCQ(#mK-=P?Voul$aaf&B_LhI|e2oECA9?
HtRNl$Y^~GZ

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
index a4ec8e64ac350d47eb766404660cf6e154d698de..ef5f30cbf20c60607d137bd8e30c4855c990137c 100644
GIT binary patch
delta 473
zcmcc5{eW9Iz?+#xgn@y9gTXN1Rz!Gh#l?b&!s_)Nb1Jy~6ij9w$<!5EZozr`o?Llq
zs&mZ$`y1=)`_5O2TU>hAy`^B<?B%oTcJF*^-S5~p{ng=Tg~is^s_v7^-*{@VtIfST
z{rA-!Rh#$T&iVb$)c@*|PuD!zK3mG1<&)qp^}Uhm|G;gIb!hIDi7jjT4g{<E>cm{S
z8Pru_pgbdrvwnk!oJ!=Bt%}EHd~aYsxAKqR_Z5eX{!F#?_2PRysjBc<kcRTFJ=?`s
z$7prAe--!{8#uGBT6IdB;Hpms5>281bAB*$oeI>F^Go?vT)Sk7KtxS(IHQetO+U*d
z)lC9gH+ER5t$MRASj~*XsKNNqu@hI<7%Y^UJn@w4f#8jzp|0oai?0?QyMC!?w(*1D
zsgv@zEx+<#i^pzTgrbS1Yn#o&$5!*V)Q3&k#IxN#Wpmv*TVu72`j7P{u9aPPKx3i)
z10^$W{%5z&C4YNebNanqLeRE%B1}7XMV+>NnQ-5&=k2C9kMxE2Goprkm73<WS<DO!
sNBJ2T*cmo&V_eV736GJ<d8|hAARekJV6;KOlE&GS_p?f|MX`be0E&^y;Q#;t

delta 473
zcmaFBeV<!6z?+#xgn@y9gW-F}iU|Jxbqn(+3ai(5Nar8qY*CwRvDWpGh<f7f+mF|+
z$?16g-}>A8^B*nWGr8ZYohWv$=yS>CeDm$K&kav}4640hlb4si{7J^AK3mVH2bOI9
zU9?{+JbzpH?A-f%pRJq~a?k2yf?fOKn~cc|*KzKC!+EEpc=@Vct4R~C3RbLI(%I^5
z740R+pT-ib%~(I}P_s(+CbJ_FpXELru$*fDNG>#@ZU3g_o+lGygY?hEaHYD;|Nbp$
zs<-RM6>>`ZwY4tiuWz|z;1nvy=Dgw6eBOEoM@z4xhdX`h*Y!^kV(QL+r`7Ph>HS29
zO)g?itkU7fU8deGJ#~c5k*&b(hQ!WUqG}<@MnO9{DzvsOTJ@r`ex231A5l?x#cVaJ
zf<B%7Hsx1*>%rq<+AV6!PfSoRiFrQx+xf1bX%D}(=Uh9#GyRy#x70hTo3<Vnl~Db{
z8gnG=<-wTSm1pYa=Ks9Q?sMweTqlL_@a&!HvTts8Y>b^2`zQ60IcmUHscAl&#mvBP
tl%Iitoq=KV4#suNobVW#oX=_`58|OI1I8N!ENPrI`2edFTO=!p4*)?+)M)?!

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
index 641142490d709545cd3b64842869f2e95495adfb..834c481872c58edceae6f77f053d7c59bdd099e3 100644
GIT binary patch
delta 494
zcmZn`Xb}(&@MdNaVPIh3U@#516%k%raj{^cuzJ16oC<C~1(TUaGIfQPTX5dKCs&@D
z>Kya`{>J+HzVnsh7MI?2Zz-5Id-?3T-8<h}_dE7Ye|7j-VX?Kfs{7>fH=bJTYIE;S
z|9y2w)#kmobAG=w^}o90(=|`F&z3T0`6ReYeQ%`tKX9949h!S(V#}Jo1Hr1kIx&}S
z26a^!D9?!EtluCarxH13tKzX4-y7J^t^6bSeZ?W8KT~aez4%^Fsw#XIq@nz4&vx<E
zF<M>jUj=@~2F|RjR-Mu&xayOEL{sShoFB|wrvkO){8D}u*DjeN5K&Vc&S)cE)6X(V
zb(4VBjU85MtKO^&Rx{%;YA`-@?8MbI1`DMoPdw#%Ab6u_sO$Oq;;V(nu3sveZTuj3
z>ZJT_%dh;`;<4Knp=e_1+GexxvDN%7^<h&s@ocwG*<5$d)>v(${$ss~Yh~9R&{(Md
zK*`LT|Jki`$=_broPKYY5VY-`2-D78QKxNRCfs-HdAsS&BYolhjHn^MRzYC<K2`>X
zr!ou-><pW?F<xfngvZF_N$f`UARekJV6;KOlE&GL3=9QD`RPT8xdGm+Y#?zaAS?jV
Ib?hJ>093!t;Q#;t

delta 494
zcmZn>XciC-@MdNaVPIh3VEEawB7(nv-NO8d!s_)M()kBDThu07taW`PqMmsB_TzPH
zaynlBxBmA2{71|8OzyX8CyJdb`do53-+X)RbHfuKgKBTs<mII=f0FU3&(`zlfhC)N
z7wwk{&)-%)JNN$HXDerg+_O5FVAsC*CS&r#b)383aNg-CUcRc=YSM(Of)%Tlbhdh1
zMSBVIr?CWUGuBT#)U49I$?S;4XSojtET`H(k_(M!+rMeK=gGv_ApLVOT&XVezkf@b
z>h1b*g`CoUZLQ1s>su}vIEBiwId6D1pSRw@(bDVa;ZC3Wb^TL>n7Z@dX*E1=dOy)&
zlZ%)Wt91Brm#KG4PaR=%WGisHA+d9os9H#}QP56~3axF6R=udKUuSjhM^sc^F<Z^5
zpigJNP5BkydhocIc8l8b6BE=+VxCX_cD^fU+QV<{IoHnbOh2abE%lD-rmcrXB~-t#
z#vDm|c`)X7<(ay<`9JTn`<%Kq*GVBfJbS0Q?3>#i8)K)%{z-jgjvDZ56$G~LV`X4?
zD#O6Q&cLvF2jeAHPI!z=p3H7!58|OI1I8N!ENPs@$iPrgl%HOdm>b~D$_5f<0>T0y
KT?;gjfdK%{G1p)K

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
index d5292ae7f5b82a3447950180afe3116e9672bfe7..17920841f7e11451a76ebd6a3bf70890651e31ab 100644
GIT binary patch
delta 451
zcmcb`eVbc2z?+#xgn@y9gF!3cRz!Gh#l?b&!s_)Nb1Jy~6ij9w$<!5EZozr`o?Llq
zs&mZ$`y1=)`_5O2TU>hAy`^B<?B%oTcJF*^-S5~p{ng=Tg~is^s_v7^-*{@VtIfST
z{rA-!Rh#$T&iVb$)c@*|PuD!zK3mG1<&)qp^}Uhm|G;gIb!hIDi7jjT4g{<E>cm{S
z8Pru_pgbdrvwnk!oJ!=Bt%}EHd~aYsxAKqR_Z5eX{!F#?_2PRysjBc<kcRTFJ=?`s
z$7prAe--!{8#uGBT6IdB;Hpms5>281bAB*$oeI>F^Go?vT)Sk7KtxS(IHQetO+U*d
z)lC9gH+ER5t$MRASj~*XsKNNqu@hI<7%Y^UJn@w4f#8jzp|0oai?0?QyMC!?w(*1D
zsgv@zEx+<#i^pzTgrbS1Yn#o&$5!*V)Q3&k#IxN#Wpmv*TVu72`j7P{u9aPPKx3i)
z10^$W{%5z&C4YNebNanqLeRE%B1}7XMV+>NnQ-5&=k2C9kMxE2GopsP?z*=xrZO`y
r6!0-HurqAl#<+@^6CNXzGg*z8fxOA{Sfv?fPu|5U#TLp6j5G!SLc+)2

delta 451
zcmV;!0X+WO3)%}4P)h>@6aWAK2mtbks8|n=uAy&{6DNO&8*jl0geH?XtwrJ#Ct=&$
z<F2f1i0l75_V3T}Iqw2T+I^80&T{i~({DGoedjUA@lt)*JZ^4hr{rkzjy*}`z@)SL
za=#i^Z?<=vZQs4-shU*YI>}%@hojj6W1+4IyX*<vh;yf^jXIK$)e(5Aq=|(~I$KH+
z4`u{YD*=C&!h<A>vNpsR^B(ZPIh8-+9#vR|zp|%E$zfemFV0*FWkjF%_F|PwMe(Q}
zBEKst({HbY(lA0*9tK0O>YojNKtVZ5#lwkAf3A;|5(0~F?ka%ig71+)vP2d_1shk#
zM3voj%ESgi25?5$7`d7iCRAfGQn?6tDz>7k=y`vxI?ni7T5fX&e5z9N&GwY~UxmTP
z7Au4%r^t{ebX@0?_Roq^mf`k?Y}U`YXT~J<W!xpQwZjz{CG-Vc#AfNiT-$lfew}am
z-3Ls{)}2BiS66GfCmrnDh_PLkUHoO@H&9Ch1QY-O00;o`h^SaCuI=cR0{{SU4gdfL
t006VN0jUEC@`$Kd509>)Z<A^TG6V96sFR-s8v&Y=y9F8sR0RM4001nY(Qp6&

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
index cd7beffd7bcada83604ca8e7d847a72c6e5e628d..3ed682f328f2e0e1cb3c118f1a6346cf6462104c 100644
GIT binary patch
delta 451
zcmaFG{hC`iz?+#xgn@y9gTXf7Rz!Gh#l?b&!s_)Nb1Jy~6ij9w$<!5EZozr`o?Llq
zs&mZ$`y1=)`_5O2TU>hAy`^B<?B%oTcJF*^-S5~p{ng=Tg~is^s_v7^-*{@VtIfST
z{rA-!Rh#$T&iVb$)c@*|PuD!zK3mG1<&)qp^}Uhm|G;gIb!hIDi7jjT4g{<E>cm{S
z8Pru_pgbdrvwnk!oJ!=Bt%}EHd~aYsxAKqR_Z5eX{!F#?_2PRysjBc<kcRTFJ=?`s
z$7prAe--!{8#uGBT6IdB;Hpms5>281bAB*$oeI>F^Go?vT)Sk7KtxS(IHQetO+U*d
z)lC9gH+ER5t$MRASj~*XsKNNqu@hI<7%Y^UJn@w4f#8jzp|0oai?0?QyMC!?w(*1D
zsgv@zEx+<#i^pzTgrbS1Yn#o&$5!*V)Q3&k#IxN#Wpmv*TVu72`j7P{u9aPPKx3i)
z10^$W{%5z&C4YNebNanqLeRE%B1}7XMV+>NnQ-5&=k2C9kMxE2Goprko0o^~Qf3B*
rQ~V4J><pW?G45jKgvZF_N>(FgAaC+IR%yoBlTWcqv8A#CBaHz7bVSFS

delta 451
zcmaFO{fb*Sz?+#xgn@y9gMp!QMFfBUx`p`@h1Kgjr1KAQwx~_ESnK*oL_P8L?Z@lZ
z<aE6LZ~g84`Hz<GncQ#HP82&=^tt46zWMgr=Y}Uf2G!oM$;(S${v_j5pRMQ914}ml
zF4`{@p1-YpcJBSX&sNR~xo34U!LEJrO~&Mf>o|A6;k?sPynI!!)uahm1uIr9>1_43
ziuMxZPh$zzW~`rfs9B|Zli3l8&vG9QSWdNnBo`Xdwtv%d&y$I<LHg%nxKdr_fB%*=
z)!X&s3OS|y+FF<M*SB0Ua0-=UbKdZ3K5xB)qovo;!<|0$>-wh%F?Hv^(`tC$^nRkl
zCKoX$R_XBLE>rK8o;t$j$X4KXLt^JFQMHg{qoAD}6<XUCt$I;ezs~C1kEp1;Vz!!9
zL7&ckoAN8Z_26+a?H0A=Cnl(u#5|w;?R;0zw1?l?bFQ7=nSM;=Tk0LvO<NC(N~nHe
zjX9F`@?gyE$}@Fy^MBrD_c?WKu9HG|c=k?p**CX4HpWhi{ge9095vwEygYQ5GBYro
r;%8uBXJFX8gK;M_Cp<<bSFsu~19_9zvr040ntYm7iY<i|7-<XuFMrJ(

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
index 8bff0d7b830258916961272d2591c981480a130a..494a877eaee98f0e63fb1e5d57eb5ceab8de62e0 100644
GIT binary patch
delta 460
zcmX@NkNMm_=K26{W)=|!1_llWwSZd@9<3_v1&j;~pO_dJc!8q1iFui6sl_FFCHc8I
zxj~M3j}3VC{1$C}&ok>TQ}rwTZ&#88HwdK)YX|D7=1#gly-zq_=8KiFO1tx~IsA>v
zvi~NEo%{6V*Om9>=WCxEp7<$Od-Lxt+w(prFFs(do^-0wvp)UX+vi?6S>No-e($S3
zA8fkf&r6l&k22@n*n3)cslC~xUZ8w#?kcla9!_EI4^~c66VrR?rs--UDaf;yC4!58
z(wS4Y1d`9V9}s>XB6mP})drsa4a+@GCdS6-pV4VGT6Erhb;QG<K$}(VC*-?Mec2!G
zlqs=Li@(`*!=w4U>m42IExnIkR-O58S^pFvrtbW_<O9VA`#lsQmADr+^{!4{bSm$)
z(Z*H<W()5dMn$IDJ}ai3^muyifosm9RWB;T=05)s6_vMns^-tMZm+*#NgtEDMV%&h
zXPywYTK75d_x-M*X&=A2n!T<1V3{gZEmbam>sF$0uh1_hy(HuR32Sm~)3oFB{1c>i
z>^IPiF6U~DiCy`0QOTy`g5Kqk<qxNK#-qf}<`s-OcR66uH2KawV`d;{ve11S0Nta{
Ag#Z8m

delta 460
zcmV;-0W<#2z5~v_1AkCU0|XQR000O8@QA2b^0D=%Z~*`S@&W(=4FCWDZDDR{W@U49
zE_82gY;96Oa@#Nryz3Pi-QkJbOmF!`PswyV2nkA<lAr>Twf*}*maSTzTz411VgaA?
zA#kL_KhnZko?f5&{qDK%JO(-6qc6K(yXToHIU0OmPf|HB>3__={alGn&Hl%3-*@kM
zss@!mon$bc!`bM7u~659UG@ZS#JN+|Mjc7W>Ighl(!|0g-6*AqCnJKPl>kfOL6TWn
z8)A(42zcV0$^&>r6_()<_B1Iutc&Y~nWa!h^!aEND_kmyNA(c-Ls6Oj_ev-YBUI&K
zun1QCv*9%;D1T?Ec)BFh-}I4ELSXUDZ47uW_z?*tOJpHbuyJ)vRM~A^Cbke{0A~qX
zMy_Us3Dq(gsoWX7h)q-#J<qE19A8VzZMHHc-)vE--%2cgY_URUaxo2gLdSJJYX4hN
z$}--*$fjKnKBr7#Pvh=GTRUu`Q9@t9MQr9DjJ2)D>?_Od32X!R7ba!vP9c!1E45sd
zPWCur=`QOo{4((iP)h>@6aWAK2mtVisI#a6EZqq3h^ScdvGt~t+}<+-@QA3B65l-5
C+0_&P

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
index 7f97382f971..ecc7675d19a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
@@ -1,3 +1,3 @@
 file_format_version = "1.0"
-dafny_version = "4.6.0.0"
+dafny_version = "4.7.0.0"
 [options_by_module.Foo]
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
index c31783a3968..a576b648061 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
@@ -4,5 +4,5 @@ CLI: Error: malformed dtr file NoGood.dtr
 Translation was aborted because errors were found
 
 Dafny program verifier finished with 0 verified, 0 errors
-CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.6.0.0
+CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.7.0.0
 Translation was aborted because errors were found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr
index f920e5999c5..c09c81885fb 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr
@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.6.0.0"
+dafny_version = "4.7.0.0"
 [options_by_module.DafnyModule1]
 go-module-name = "GoModule1"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo
index c09c1487b37df9342165bee49c573eef360bb18a..88dc9758460e993a31e9ff00f354e4d3c1e5fed7 100644
GIT binary patch
delta 489
zcmeBR`M^>i;LXe;!oa}5!7wB1R>ac}8t2agc`1wx47?0747rJUnQ5uTC3+?KxjCUB
zoD9qg6*Xy!KwMhE&A`a=6Q~ZXJ+|M`kJ*sN^}D63X|=noL(<V%qT&pp%G!m?#5!Y-
zO5VCRk4Nb8p>KQt>;7M1rFzb!HqbQe=H55;Z5Q9OiyNN&I?wKB`u_Od%y$)!JT6%n
zUcI`{KJSr#dd-K&5A42NvD(xu-1^QkcDLV*-aAS%CPFRB>!wG=o|vezwoxHyaa6>O
zQ`6Q@`FP3q)egZ0lIMed>6df%uqi%HN?E|vdMj{oF5{WV^9|zHKFQD9$aT8r@Y<vw
zEy1ao4w@2y8Rp-uPoJ+UaD6<9lZAWj<@m2}*}r_fKk=80stiLxQGR++VlLR{GTT_v
zq%nOyS)MUHRE`-}7)k&`lYs#kObkmJK`gWoWrc(&T4)A%Gcw6BPy8q0imY7>XbRjx
YK#d>=VQ6G!1KGj^gbRT5E|A3x036Gtr2qf`

delta 412
zcmeys(!o+6;LXe;!oa}5!LXvUI^t8yL&oz!UJ4@v122%yP0Y(oOD!(ZE6LBziS2jv
zV>aY*{ch=MTJ0|D@FrsOBc=seDXQnLC~aJA;e7k{WXGha8~eWRe<~lk{K(8@`m2s<
z?Vf(u;Md;=N@_drT~`19=KE^Hv$Fm&o>J<|cHR1Z+_(PE%O3tZnLF+CqTI_07G1Di
zo_(Ej^Tg<uX1At-BVU77b6ZYYVk+R06~fIOee=^)qqtq3vgS-Ck0ZVQKh<lzsE`uV
z!xOR~z&dM-ZiD4($q$F3{v9?BOPra%Ba~-;!73eI4OOnU&+5{DM)I%Ah%stRSXlaN
z^}fFi`~FFTysn7wyT54#e=^X|6+p}m#05q9=|zdTlfxO)6-Ag4>d?aosFZ<W@_j}z
p?*MN`CS;Z9CW2K0i6xD{fF#uX0B=?{kOUJD769ocV9+x#004_#kBk5S

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr
index 62d42175e4a..a5ed5313788 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr
@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.6.0.0"
+dafny_version = "4.7.0.0"
 [options_by_module.DafnyModule1]
 python-module-name = "PythonModule1"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo
index 276201070e3389fa60645f64491637a192fd3142..273681f03c93b9faa1bcd0c19b43d44b2b982f8f 100644
GIT binary patch
literal 765
zcmWIWW@Zs#U|`^2xR7-#LiDQDk{m_`hObNv47?0747rJUnQ5uTC3+?KxjCUBoD9qz
z6*Xy{KwMhE&A`a=6Q~xfJvYcP@38^Tp5LOa?|Ek3WvYIq|LsbW;0B>oVeLRY)!a$<
zr}u64llfw0tkUlMYYu;-vh2T!V&^`6`E})e`T5%Ch9`c?)!zJj%l5p_$%_w|t0$dm
z^i2Qu_PJM1);IgI-}|c12b-?=^HQbxqs%!s_MX;VYHv2F7bu^byUOg9hf|pQgO!ui
z#Pl++YP;G<3iGUEiQwX&bmsJ`0}`JFKOC`~%Ko84OXslio6Ml12=Uw8#@-8iUVOf&
z6}BTpr2m!Tr}jlgcdJyVv<a^IWDvoo{qN?7St3(5huFj}dinpg^3s+Ak7nPN_z?3!
zS;%AB38xhak6+DLvFY|MpB%*#4Cj=#{fRltCA=!tC}^i~h2ZQJT2=ExpIh#mHtlgv
zs@J}oi-Pt~jremTsrAB>B&km=eXnb-{@cE2O6s1y6Mc8b)%eXkvhUd4_HAW1To$+N
zYv{gl#$F;jy8q_=Q#q{P#nn=?{S_yy?l)gL`EOsuzSD=kH|Yn!qwHkXz6j-Q=Qafc
zBQP0=*@013P?Voul$Z;StY7yd(poSh>+<#R6CP(zp430Df6DWsx9937j~<;m>#up%
zGqk|d=k)3?tebg7SM3xLDGK&B`V=f;<M8UR<115>#zhK}tgTIp&g>ClRoyU$DI(~k
zlt$p`(9^680p5&Ea?H3Ak_6Cg3=F`u!my+f#6n9}tdL}dmZXr4#Ple#k(+@g!@UhO
Y4CHML!&uosHZuX?0wC=UOyCR*05L`?eE<Le

delta 548
zcmey%I+e9Pz?+#xgn@y9gW+V>z6kgIylOd&3=ChH7#MhgqPdBAnQ5uTC3+?KxjDH(
zjzzZ(c=o&&mAw0~^R`d^PgnnwB{m$KUNa^wV4Ae`?{9}`+R^i3%Eb>PG0y+2Sg_=<
z{iQ>Z^Wx_J`ulF@dmA>(`-}B=$M1eVQ`1taCc!_*(%@zNnSFm_I(^UnJDzvH{C(vr
zwyE}WQw-)EzWJhIW5D&6*l#R(M|K8Zb(8fx@ruJH^wN<-s%xv3cBm&e9h}PG{m^kz
zWu&M?vK`Yri{+mf<N{k$D_U%Qz4%@yRVSutP7$oNi#p0Rz3Wk+t;@fFkY&;9TP_(m
zh03v=PB>~W9XGkDsD4`4a&MEr^|ec;2t?ErOEb^ou5)2JDHO>eniC@{99kAVy;GM(
z@<8N~Y4cY{COU2PanmYi(@zo(bv?iNmCf<%mx|`B^*L!C9r9|sP`7;a8i83cKF;$l
z6wY0L>wnmkO+DMqH)US$KCe0X#`PV)FI?lBoiXKtc!A*TpX|xGuML08MbBLO;NPJo
zId3&tioSkaR<h~7;OX+nA8{X8K`}FV0h0tL14BVketJ=2?&L3w;Wi@7xT6agV_>kP
v5k#RxUVt|vlgQ-xOp>|~B_MK1<8)wLLk$n`W@Q5jG67)$kmd&_0R{#DNwL`e

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo
index 48a3b05a68d8130c4a994c7386f54917597a6f92..fb96ed004fd51b5a198473d0aaaf84baafc63921 100644
GIT binary patch
literal 769
zcmWIWW@Zs#U|`^25Xin2A$rwnNe&|e!&fE-23`gkhTO!w%(T?v61|fA+?>!5P6lR%
z%9=DLATF)oW?*Fb2~-Q#o*U$t_t=1E&u`Jz_dK)iGF89Q|8^xwaDz~)uy&xHYVM@_
z)B862$$YUgR%v(sHHW`ZS@z#Vv2&lk{JQeK{Cw?m!xKN{YH$9%WqaP|<i!Wf)ss#&
zdZvGS``jxh>zjSq?|s$hgH2cbd8yL;QRbW*dr#{wwKtp83zW~zU1j#l!zs-D!OBT$
zVtScZwOwr_g?ZMoL~!v>I&*r}0g2CoAC6c~W&hBjrE^&MO=eJ0g!pZ4WABAMFFs$?
z3fmDP(*H{FQ~M&LyH%=F+5}g9GKgT){&(}kERiXjLu_Ifz5M@Ld1=dmN3(BBe2Dp=
zEaWlmgwu+I$FF9r*mQfBPmbaVhI2~W{=}T+5?+;R6tvU0LU8s9t*UvU&n@>&oAx*-
z)ob6)MM3+gM*O*v)Oz7blGLY`zSlKZ|7~A1C3Vl<iN3qzYW!v%*>~)2`?j(hE{j|C
zHFV!NV=s{%-GB4`sT|ht;%cec{)!V;_nR-B{I@S+-|0i&oAd+VQFbKbc*Oq1j|t(x
z2+Rj!c3_kh6y>KECFX)7%OE2;?N0?pWL>@<&T;O%?^kbKJx||{XZ<zLdS3PRT>a$H
zqf@NK2R2m+WZHJ@aWb9W<dm1?=~ma(<euf{S65LN=-1Vz79gUsctJqGl$qg+7O+eU
zX7JXEWLC}EnYEK4z?+dtju}^Ck^s7ofdQCa7?w1GSZGO$6_T{jk`=O%n4U#8ax>6m
cxYvP(fxM1k7%LmdW+ot90HnQviJXA}03QM+wg3PC

delta 570
zcmZo<o5@-q;LXe;!oa}5!Ehwwc!c|YUbP%X28ORp3=F(L(cHwm%(T?v61|fA+??DX
z$D-Q?JbPY?O5T0gdD|!dr>p<T5*rRquNjjTFiqO}_qW3|?dW+i<>CjD80UXhELd{b
z{?ehyd2#c9{e8Fdy$ze?{l)sb<99!wsc9)yli(j@Y4EcC%)Y-doxW%P9nZU8{=RY*
z+f@6xDF*Wn-+a-qG2nVj>^GLYBRhkyy2*N;c*S88dg;g^)wNYiJJge#4o+q8e&{%<
zGE!6`*^X(R#qv)Ka)GU>6)m>DUVN{UsuR;RrwG>CMIGgu-t{QZ*5zM7$g=45Etd?O
zLgm;_Cmgkxj+@+6R6nh2xwpyR`r0K^1R`pRrJ3h(*SRpA6pG{!&54l}4lRqG-l@wX
zc_8x0wE3$e6P>pDxM`KM=_d(?x}M+s%I5g>OGR_m`kXY64tcd*s9QdIjlirJALn@&
z3g@oB^*?ONrk?HQn=-F=pVypx<NA)@7q0Qm&X{sRyg+dFPxj>8*M`6Cqi3#t@bA!)
zoVS`RMPENIE7^2k@N{|PkGK!4s4=rY@nb?bFh=r$m>q}<it^Ko5_2biVT@K3Va6SU
yK&1=}lM9%{yaT)$nUGbYn+R43B$hNz2c`h1`2pUnY#<3HAS?jV!oY;VzyJU-?%Wmt

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr
index 17ec9a85dce..e495416f648 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr
@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.6.0.0"
+dafny_version = "4.7.0.0"
 [options_by_module."Some.Nested.Module"]
 python-module-name = "SomeNestedModule"