From 082caae4981e793a8986b76d0ab31cdb3f8294a2 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 12:48:44 +0900
Subject: [PATCH 1/7] Add support for let_in in Z3 backend

---
 compiler/verification/.z3backend.real.ml.swp | Bin 0 -> 53248 bytes
 compiler/verification/z3backend.real.ml      |   9 +++++++++
 2 files changed, 9 insertions(+)
 create mode 100644 compiler/verification/.z3backend.real.ml.swp

diff --git a/compiler/verification/.z3backend.real.ml.swp b/compiler/verification/.z3backend.real.ml.swp
new file mode 100644
index 0000000000000000000000000000000000000000..b079121a62b355df7eed65f529a5845f7c19f5a9
GIT binary patch
literal 53248
zcmeI53zVf-Rp)Pr3W7|001hk|PbxxgCEe98z}TH;sPrQ#=tt;RfTB{lb?d9Do4$|A
zeROqoIv^l}0zP<UIZKU*FIIfaEF6dfIHN9cL{WnZIt~n=C^IswrGtPdIP?4O^Z35+
z-doibbPbNyP5yoBevk9mXP<rc-e;e47IvSTIqq(n+FRlC^_9wcePZ$O-%dU1i$7SY
zEOk4rm8^S7w>JAsueY*pqu$$jyjH)Z(>cF$y3w6#cIvfe`K_161b5xh>7L)!%~m_T
zUG-YO)~xNScUr5BX4c(xfuxoiTy1pPyDsfpsMXJB?Zv5XR%=eRh7v3%zx`{Q0^1bW
zhysKD($1S6U)i^J&u%?(-Nd!-o4)bvMo({F-=@Ge1-2=$O@VC+Y*S#H0^1bWroc7@
z{s~f`zxue!%c$3*Lfwvq@2iHs9~XY#9=?wc-T$ia`-S2AhllQ89ezJQe1CT6{#S?J
zcZTohh62QLd`-As58n?A-G5BDepmRuDpV-G|8?Q|9pSq+bpNs8`b_x#g`xY84%fda
zd_O8wD5n3l;reai`w2t$!{zO-Z3=8tV4DKl6xgP~HU+jRuuXw&3T#tgn*!Su*rvc&
zgaWn2N<}v8as9*mf3*MKeoduP1AD-3@bQ09seC_pDYy@u1Si0w!Mh$`skFh<z+=JJ
zg3n`ce-eBc{2usC@G5X8m;=Yav%u$YEPNDvAD9CUJd82^-QWy(9QYNC>j%Ip_*U>K
zjQzKR1@JB4FEP%46x<CCgTKOA@LS-gz$|zi_+1<f4}+J1DezGo7WacA;L+e0u-6;l
zI5-Brg#G`1@NV!H@CvX1Ccw4e1JLVd!5lE!sr4M6{jT0=_p^(Acd*jT`mVOPIDcv1
zg<98D+qG84{a(M@XfIE?>IHuE*H^Pemt9=#x^uPeRG-WJb$^{d>-~#)f|Hhhqu<j@
zZnnQZ=lUJjU&&IAH{38;sorpdn@yR{DSuwzp;m2mm3-Yo)?drAwwqOPxZhs1+lMR;
z!%@&iZK0XD*$Z}0mAcod9BYmKivE~i8no++S-t5FT9J>}R;S3sU2sc_x<6HV<~}R*
zP(|`OK_thg%B%a`Q4&5(!c)p&URn4mk0(^3ZY+<bq#p_$aeBShwJ;JlyR^7Dtzr_J
zkV_=ofJR2Y7w_}!-)Os<i>0VF-CAwksa;gf#dT;-Y)iAb?iL5)0(-UJt+jhiU({}P
z&!Ay<1~gm8t=4+J`65@<x}8CL(UO}Lr7!Jk)%x|7-e95E@6GLS;UY{nsM`fKaJWbs
zT(33S+;Fw77^k&5=x08;z$88YbRtPg64oeWun511dAVeTX|z@|k^4gC__LX{vNjLU
z5<6U@?;2K#Zno4R*G`-I*NNyMXMWVPDR;Kbo&KQBrRKU%FqC;NaW`qy+V13`TC3@5
z)V5pmElp$hJFBj<q}$LY>o(U#+Cw+qXeBF>7mB`k-wtDX)xW<2l?UxsXOWmA3e#VK
zy2~q_L4UYmrrep8%#y27jK~T7tlLs6y?CG9cO=pb)E58Esos&sbUdqluV3r-L(^Mt
zCE-*@wKDBP7R{y=!Se$}YluQLwRoExvv$3+m{F2*ha7=a-K+<_X-MDSoIajjG<LR}
zb=}%ZqrO72@MBN6mW}>hGJ$HlUEolAF=x$2mwX%jMy=Vn6dIFKaE(gPZaeh0Csi|R
zFC!m(Bh<Rx+Iq#(a@8B$v}-ncecdZCAWay_99iMT`%DmKy&jc>1oir$HK1P@e|lao
zCa~WfL2OQ$>{JE^e2%+a=DDxu+gWTqpc06-<{<MGwL-1ds9qp=?20OaD9i7j3Y=aR
ztM3R@Uv$O;{Q+#wLuBg<XSwWmr{UzO9{;!-@)Cx^)gg8_V*tqLCraE`h^`7*qbR20
z(4f=p6$*>=b_$=1oag(ulMFXG;nV8E2dka7iVsgZ6=H{f%{Tv=SlAaf2nfV(Uf$Ct
zG)|D_l%#s3DC{<xeAXVc)I?TNCz<A{QfkCaD$vhbtDSDGyPk#|+G{y$ONhYkYby*<
zspnFi8Uq+|PO@P{>`@6u%{Y+m$f-V=MyObqNC!$>Xo*5ANXXE@TWA7Nz(gKBa;xo-
zN}t4MsR53V<Ouoe2z&%hcCjY8YJE46DR$d5Y|~Kdxj;a$_7X7}OklnK`p#9xm%jJ|
zxtBG2p4K&rX5Auj8XTf-umc_~@|B4@*IREbbeg{2hyl+betb-I)PPZL8n5HfFKDev
z2fL9$k<$u;Hu(-zc9OR7Vli84v^93rvoyRS$l9vMJp+P9=?6xQawWo$9S7vlP}PFS
z6x&Af^(MVEPdS9T#KEv!n;qjcmJyDF==DaAVJ(oKFOfeKOwua~yjc7*$b|wWOh!qe
zwEnN27~Wm&c9y%fmKw-L4fXo+FcFHc#3;JH=IK0=MNmoEKs>!n>N&Z+I1VlByTeE+
zeHSE6M!t~1fr`3dOb+Gn-bw`q8^E%sVBiM2@4@)jJi)=O=2W;IA4~i|y5fq{UgxxA
z&%@RS1IJ9ETiXN2Yv(gp^{-7<I;)5b)G+&=?)Cj2hY?M6|L5ry#{9+kTD;}SI6vq&
znmtqAMB8JHde-itlK8F_emV_%y4_o)HHlAl&02eTP+QL2a)*%RwrGz6)M~`R3n9{M
zv>ILql9GX50^Qvm)2B{NpExsf<g`0^${jj+;_%FwnUg2@b<|Ctc#(Vl%!$JcG$`8)
z+JWv)V=kQ^6=lku&TQmRT8oT&-Nu46IG=$PF&3FYzW4xA3XwN4ecH{Oo^ZEJpPo6r
z!`(4+=C+e(&nU68?Iw(f?2rOVf(z>oi=m0SDs!M&TT>}&s13eT((~53s0Quj9gH(e
z{WWN7L|p0jSNHGQwYIi4Ra>pqSF)*2cX=1-h^)O`$7T*4IdS^P&b?E_p^|NZ=C0P)
z6}mlFDg6=w;gF!7t)f7-;Vh9rdPm@kVr#vqGhl#Ncbx_4PmC7z&MLn&IL9U}(rDUB
z7VqqE=d!Mp4o9gNN=SGjP;p}NfLjk~w>y0+a)@_#M?-wPySe5g;HP4M`*Ry@%qV_7
zNBL_&>2>O8QRske<QOKL*9yHl*QJm2rraS)+-)qc^j-DPq}#iD?_M{fWPJa&cJ6fd
zqcYNSBX#&*MV*YQN)QZ6T*34xK#5^}R*7qkpKBK@vi~u|D`$fJ|9si8d>+E)?}8)X
zYrsR;`Au*$*bDZ6k7MUQ489k<4BP>}4SY5D5Q)AOoB_`Tj|U&Zw*Me_75Fw#1z*Cx
z{|)eJa3^>&_z*V!uYs3>z2Iv7#?F5)7=UMh4`S#4XYg{c44wkshn;^vI0v2xo&es5
zt-lU-2Als4*!qWp&Hu%#vGKu=g4;m_d>GsQZD0kQ1Uo?$Tn|14jXnf^1H1<GfarD_
z6hAaMAC2XQ%-}NZ&NQl}PSe|3@(dtDceqRYkjM;^-VXMc_0wKYssKYDP6BCMykrKp
zWV!vJs~QI@&RupVIt-CJ#dMcZ>yWtm<uj7zXByOK%JUsMSSj^O`*Qt6cE8x(vT*j9
zHI;EW>(4h(mAcCqq4RP_cq><r@C3Q%w<`7?|AcYJWO~rAc?w0U%?K3rJuhKu8l9xV
z22pHD%$_#IW2$w2Ua}9V8!2*WU+}Qp=_an-Jux|#^5n&dYbTO=9WA1=(c>kN^tjlW
z7}v<ctLA7SNpnOhvLYoP4d~W&Mi#75FX646)bozawIwWTrgWqcBvyA!Hapy!h_=vx
z5Gcm0jr#diiRxw*SFt1U4+q0sBq~&49+?w(2TJJ$OS)>@5p$9G7Fq*=G;@86VWl^~
zP+s$P9^xif2F>n>3aCpqUP{32r0UV~Q#;OM|D)E0X77pA!E8hYlhD<}u_%S2ml6`^
zkcb(ctpR4`LTa$l6k}r5RE_n?Qfgj}E!Ijb71Y_hCcelqH5GNZcqn<D<#yu|gSHum
zK|ju^RY*4x-!a%pFOW4Yn@z3~6t2(${E_Xq(nd}n*27hhz_C`g(78q$o_>@RV49F|
zjD7{LVY4lEFtW{cFlFPJYpvTDN6Q2WMR9!pMku8YN_Srs=eX+eTK7C^2~HILK(C*S
zf<g&c;iRh-pQ#Q@MiV5sH|+8BK6YMkq~72XPan$rr1Z|zKP5h`#OBo~@_ll<4(Gb5
ztJUo%LCAT?(xXj+rkpYy+puZ)%?mbLpNrxvuTE}pAFN0@ka(Z(bmzV1J#V6T*kxL^
ztN1*kiAecXNaR*D&rOd{xvAu0x{;!5=+98hq8U-7BaA+)jBq5H87${<!}rNhIo*v`
zuYVLlu>?=K-hebsUS}8S$UV27A=7cZqzsf6dL=3hKI$=*#wppCUqCMIPT5Zqhk|i*
z7sFn5XQtch8ts;9ji&jkCuVsmdUNLdeH(X-{|BqMA5fepjE1oC4mXWHyVA<~jr!D#
z_nO%-qY)?<o%T3XKikBl@$O2KU2#N1$2Rwu>)}Sk8CYx5)ztJ-OVz!jcPcg%Ty~Te
zX?NCw_?MB3wHQlosaL%`Y1Aj9$dsrKSxtrd%j@Rm<M@AOy4&rn+3!tgV$Y1H3M4(b
zYW_y0xp5ldp$!ue$9hF%Op}`s(NIKgXUw6td1n5Z4f8r}1GbktDs#DG`QB?;1{qAQ
z$Kc6+Qj<y&ZoVn*MaroMc;%^Ywns&>29ZA`5J&oKA4|54k-8{(Nq;Sfw4w~K{!q$!
zPTW7};suqAFEM}g?}ct3x}{NMwvVu3ME2x7JP6Yt5MryW4Ly*xrZsN$73bXZ;KV&U
z+@5dW9ds&qTFGcELkBfiH9bLUsyU+>zsL1s2cs-7fWq2~@>2I2*m}M$$5CvpcW<>+
zROA${>2lRi*&<>z$B{10<8=9<$2S!Mym3}uWpNo=NG>4c1@?tzEp$`&^_|t)<Auox
zTb200IB+am(cro%rYf=$ts&<c^LK$4MtMuGZNgv4fm~)VUPA0Qy>cMyqemr6pXzbB
z6Q_<c11HLLaUgf1lD;%K8THfjj<l7Nhfm_`(R*rj8>*6~5(FsvUD0oeLY?cJF|F#M
zW@Ac1pZwNw8q7|gI6ZSl?wB^q#@A7FI%{)o;_1B!SG@(9&}=MBNdnB1>4h;R+cdca
zrV&D76FYZ4XJV*g2y@zWYRTMuOKz#vSH_P2_w$b*ZeqDjXSuKgAsu~N@_R{Y1^3&$
zX;3+HnM<``iCIDtMt*$okCT=+l5+Z2)hdT&GfLUAL>EodlKp=Z#_NBO4a@w0jNg9;
zHh&N715;opxCVR%yZ@u$0k8u0gMDBEd?WZgw*N1JH-Hv64UU25gQtKegD>C<_;v6Q
z_$e?8X2911#R9ww+y^d$=qLD>{QZCM4SWE+0=xh`56pls;ve{F@DgwgJOO+JAHkc!
zo4~E$bNC0|2Ij!iz=!b-yaPM{z7w1T`@z?Pzr<JY9`IeD2j;-z!Jpzcct3b0I0&u-
zUj=^eYU&H7!8d@b!H4h{ycM*;i@+i98EE{QK(zjO(fiB%B<@LO{t{xQQn*aly4}3Y
z6V}xG{oL0}+7n~?j;TpD6EL^mO($14mI3lxs?ti0xhm-z%t_(IlC#kUq$ZBjPJ4)<
zqxMxSP0=rr3YmKUEzC(E^qGdFTcWShCC&R+ui*zQcXcl-y_gXnOH|BjOzE!rxeUj|
zk=zw27gOTJ_c0WJiBxIxNyrp4U@pWP#f8^Nz&f(#*(IjtZMxBP0#vk7(ZTbZ3XexD
zi>{R56{L}qa=D2-f+vd9N*q;1D#@5D^ObG~ACs#N$vxjVC}1>Vlw#&tDvG8dNjBVA
z-iRx{@JM7?q1lS=uWGS^|4e#@nOs}w8i!;<*U)@MdRt>DpWRYlt6>}wwZcHPTRN%y
zjrOV1m28k(Ebz)pS6AnI+3Nmuvnoy+%Zg$6tOhpaMc?0oFDP8D^}=vE@${M)RzsdC
zA(SVV2mXrnQ+XlukWb8C8quTt<)DB}*)Qo+m<bX@-X$B=G0hHCv#I5&9hw<QSIxj)
zl*){{gpiapBHUs!#r)*6{nE;c({p(MM4EntvM8-<Xv)nFN@X61L6yzW&r`!JXbnYl
zA(iu#WWER6AYBXr5gkj78FrNO;&wZ-P8ONcfhSCHH#-?8LQk<VKEOqWtfnFroMX`~
zOx7$7n%<%>(0Z;k*%|yNM&Nv&F}t|Zz|~2vHowhGk4<pfR2<s%SaaTzV4S+WFq0hy
z4Lv``vL9ifYVbK8L>rq#A3UNUl3Y^?epKWHZ+ffT%yHRag&-H%+SoHaKkh`ORK?z^
z6~0MTa3FNnf}gJFry%)_E%Hs$!@qBhx)t)Er&f(HON(Al+-Ur(_TVsyjY*eXKk4m)
zf@V76<<pq3fM!c`;RM0dvx$%5AmYc4DJCFssi*9>>O5o`rEFxV31?n-{0I}@o%Z$p
zV8GLjeg6*O0_s?dv65oQ2d2#C3xnP<{8*-rSM-qNiOI=)vL@97IV3;F35*Iq(<2?e
zq`XTwm1k^HqOq=98|;?6<{nE#=p=cIiIYmCtnj#m)=;st>v_m(v$7ai-V1fLMRK`H
zCxgv>pj1KK3zncN>(wVL^JUDe<f%3-3hopMqVvUS7u7*m(lW>N-a%W$!tC*Ji=#c6
z)N}ukrR{vUT~9V<xG?06uEJ5w-&mulx{|(Dyr8#@$Of4IURi4QO?ZA5=`5ztGJ%97
zNY&+ft|O=?_|M-Kt*s2D9uOM^I*H7okZ_wX*HJ|a8n>i=(aRrld^YNPjKpQ#bEGCa
zcP5L|RgE!}nK9&2JI}=P{ZiX2dtvTSIUBDq!0fH)S5Aj8DyC`<_0D3&62)VNN~K(s
z>QY<&3u`4$4RdJpiUY9T(uAmg%Gxrjmm732UZ>UNZKCk-jeoPims~q0ub+98qPn5q
zJRfX~(u@TUnx@L_P;pWyy4Oa?4-d(Owc+rh_k*9Uy)dsw=NW=bkEo(T;FpM=lhN_X
zx1Rc{c~6M&BF<xJi69g-2J^bXo)?(YF`2)ZX|~eFNCN6Kh{eE_e=X}u_CKa=<=@I4
z#r}`$?>~aA|6}0QU==jL9YFqoM}bdb>wgS91l|cU@Fehl?0eb&F9nO>M(`w{bpa1!
z-+vDnfF+>VfTw}aVB5bB{0jI{@NYmJXe~emd=eY~W8gv121mgz@YmS+iWB(v;6Bg*
z3!ny`1pXYm|9^rX2HywHf}`Nuz^Cy6JOI8Q90fOluLFO8{r_LUD}j6hyTE^kK)(&X
z6Wjxy3BDOT2K*xS|J%SCxB#vPe}w)2y&wZm1pgb`|Chmo;D^9vPzT4r)!=WS{kwtM
z;0M$W`Z)WD`K{9)WTvn|oSPq$FGM~JgHnhj=<lVUMAbCgaE@+o68MRqm6;#xh)|es
zW=s8fI{&z|qF@-B)a&nwLPbSJJG9V-{+=K&;CDYAQSIX>?o)zbSZ>zcO4ep2nWhYQ
z*b<h-lA<Ym66aVw5#@rJofnc%R>r;!iOJlIYAhN;^o!{sTXR5(RfVCcgOtXI5pl&;
z9DbHA5A0_&_0D}qWI(o-&k1-6s-)3dQJhF4G=O4z*`|54Fh8e1!}uI(rOEMu_s)*>
zvPW|uF7dEgso*nSpDWGgsn!xBV`uClNj9Igi%AqC8a;Q9cjco&$j?0ANX>U?pYuU8
zVp3)q<HTJEspeXFrf<JXqB%INHNT%CB-b;ArJ~!nxVGZ8?3YxOGzvwSJFMsj7Vx^e
z`8n9TmoK}P|0`L(Vv+S7j^InFUm=ij3WLq!tR&1WpLw5&NqC+NBhs-{z+g0AcE@Zu
zFwTAibg4?-D>KFnw-|ch@J!4R&A(^>sM+vf@d?RLg)&3Iy&5BEgpr9D&GJAOiW=uV
z%m7F+C1KvfZ7|m~wq1!EY8kCXPW>p*GFZ~FcGXB@D4MP7DglKI@~t4uD3_lkYDLk4
z`b2M`;u=ktnjI9jln9-S+1sX)@prHttRMyA$JwG-@?rpuCxm90x-q-Ln={@Cpb4M&
za*3T&F^1}BiWwE*eb@Hs^6Ll_;_F8+36)i1(IKWUJ(k#hjKK$2FPH<TI4y<3gmg(w
z$s9FGMPb@%iCOI81HSq;zqR1Y>4h-Mo#cL1Yv#icr5Rqy=BkQE=7!uYX1kbM)!S9G
zT=(;sLvvSl-HXmNFRJ%^{Irj|;TegK5w`Xs$FGYEGPEa-3xCG}%l|C0WO(3U9)qIL
zGet8M`N8%4z&tA^w$L;*P#h#}pKs6_9UtY%+X{uUY;>)f236C?FRGm_fbQa?o;MRi
z0=i%w#LH3+3JHaYA72FZ`9h<na?Pi75IVMqYtvY<!h2TY*jHmU!w|2_g-7Yh6Rq=v
z-Q5{!6NnIAk3`_PRC}AqG_zr`T<@svgm-g-#J9WIh4LH3nk6NvKz(}?4~Mn)>|E4Y
z)ChKI$;QF``<?xf=%o9~yYS3b6s<fMN(oro&dciX*@rBA|Iq`d3wDsHGUK8}^SWCV
zeU~ZJaAVuj*S%Qf%dpwT;grQEw_@g1H4n~2Z$)*{$0}Tynu_gQ(amC08WR`TD74ae
zn=kKn(v-}j;`?YY_<Yi#KaRwnc^aD)ne0<meHa1L+y(^<69_$ZMQe3+GB4x`Nt6`M
zykM91#S)FtIE~50{Zv>w+>oN_-y9W~nm#V%EXhfU3PEz7?g{`-Y9b>>zjoe+enR~;
zum{R2L@~yBrbw?`leC0GL1uepmC#DQsa`5?FM5dy7C#=0i}&)$N8Ry}2YeA$Z!4?K
zDP{j467AcXEBvsU6nls9V2~CHye@F-5Rc23Rpt|=p4hu6Iz^MxaA4U64!1ImbW;oZ
z-cSs2*CB+;1uTdl-9H$X(3XN7bprtd38Kh^MSMpLw|t(KvLuh}e@xuU&&lq@{;$jS
z<nu0U{MUme@IvrBZ~%N78~<VOULd=F8E7AX<KXGw6WIBG0^<DtIsSeg_&e<UKL@`L
z-U%*)+rcxzUtr_^68Hgd5%fR?t^<z&SA)O8-hVszS?~b31DpakgPq_{vG?BzejNM|
zco8@Vc7w+N#REJHz5}d-8^Fh~_dfuB61)+-7TgAQfNufXN8sJyjo=9Q9QOX(z^lMT
za4UEcxCVRzyZ?8=Z-7^W^WaXf5B$y5+ygHMd%>S#^D92!ec%VcGPnyo3uu3Vr+`18
zJ>(NmyJ(*Q|50N)N1%N^XwbSxj!DDvTH~Y~*tum?Ju<zzicfP1b~$oVf3Z^fpu08e
zzX&tv0D&j>@xlQ~1NqoyvpsWmB_%Oiku0pbTd_0HRt3L2+j?0+=Vj<$wgJ*4GB#Vb
z$7SAoSnPjAgT-4fDCaVjTzk^p=z=pW_R2!~=){^>+eoLTn7)5x_(1FjzfFzJXZUB^
zgthuGekN`#XpIr;Mz`<T&oXbFEIyv`E^Z>WR*7J(F(XiX@|iJhM5qKRuDcOkQ&lH}
z(h6%m+pK9$j~6V&A+yviIed967Fg3fY+6ulG#N3@hEm3xJ*8KDh#fCCye=rw)22P6
z%|xq-c+r-U^=BE|bKd{R(^S9F!}(KN4K1P?wv9YS$$ig$X7NSi018ypgiMW>^ie^5
z9$zVby&}6Zfk8?C5wYtSZX0IdaV#XBePnzcdAPtfvYxKM&pixg7M00$;-~1~RdXqS
zSv)+NT43g!G5=XJ@Ublj+~x)X*ReEI)6===BZzX5Rh{)df#u0Ew~*YM>8IB6L=PB0
zNL?Igg3qp^@_0{BY-HqXE|pAe6Wc5`Si~|c+a#RANF#Z0Gvk3RyHD=PBq6pg=UvI=
zH9Ug&aYIrq4FmeIMM<?)sri+WXvb{u%?Drxjni6;EN6#8<(BA|k=j}STI)7?isT4P
z5M7(Yek0r^Z7nuq)il0K(g=%w<@Oyn3wso!Q~|5zzxM`FXB8Vl3PiAWLbH-k)I80j
zkvze(wF7QpPL>rrf-qLp@JL;@BweG~oTnn139g!|tu`T{z0zP{!7C?SO7{w>?kT5g
zY+^-<gMw<6<dNMDijtWTTFp6bt|SeD_OKN>RHK|9niU3kT9iI@MDxXi_Cn`k)PLy6
z)w6B+Bo<NKI4%p3czdTe)$Yve$9=`;qIEqcMRRJXFvaJGGtRV!4*N>YT_MYuMs*|s
z+R2DTp@;9OO>ve&LL;p#_n1!EdGBVL&7FY*#<3(Z)D{4i;u_DV(6GqiltJV!v67ev
z{xf!?lGZR`1}e;&h#jko+ALs)J3pCs2QIS=(wekMG>9IHZxpt72|A|{`uvnRK+DTR
z$kf~Gvz^tsIAKFEZ1EjiE~!Lgot}DpW1nX(icMhqm0-ml%nEoWZ``SDwONY`=V!59
zv);VwI%R)O71h2uzaNO1_(~M{VdN}oh6T;Ca5+v|!nLWdiz0;xd28%AAu(5M>~n_@
zBKdp8It)c3yRox1zN-iRqXcq&6Pd<%N7P5g97kB`#Vs!a^HNOb*)C+NvSm(}Tai+v
zussE%X<CgaKmAmI-UfvTVQZlrUZTX=E0K{a^kMJ1U?R>>?p_$N*~^cLn(8uXkF_WV
zJ*Qg)(9t-Ni6N%vZ7#Fql<;}s7-3dc|L#>Pvj5LxgKLjI+5d5W`;TGke-Qi{xCmYV
zZUmpj#(xL62kZo2!nS`Ocr$nnxEtIBCc#y}(v9Zp_V+dgwkfbpfo%$GQ(&6{+Z5QQ
zz%~W8DX>j}e^?60!i%43A&5y9VRS$+KZOa@Sc*;vJzsd#Z?;#Q(67W4ukf5t*6b_h
zPV$L3&7<j4$V8L>d3h?jTiA^$Sb!ErYqKxor&;FhUT}*Q-?6Ei4c@VPW8Pr`XoEL2
zHRPvra3+}L9QNqL60R~c$cqP`;|N8h(vxo2OW1V>Y8P&(m@JADy)U~XGfQW9@Q8xS
z*j$`dXXLAg4><P5B@|7+loY>x=$S59P4DxLN76XVtpOhJP4^2)PiX_F7&z+7aB}qu
zukyg?ThqN>M(Bp^kdYke`J&*$`r+ukvRKpP53x{}VTVZcyU#hBu5Gi>cz;~Hm)^u(
z!(OdnQv_R*#`YM^0h>T?;ED)7TJaTY2g4rYkP$DVxgqq2+5fxfe_EF=`~R-c7yl4j
z|7XEl!0liLd;xp^=fIDEKDZk!fNud;gU?~_|2FtB@crPq;M>77z-RF<XwCmG1I_>6
z4_*ge1fBt&0=~dJ{~v*001dDJZUbM`{66?Y@Sng%puGa03a$d0_t%`i*8cAWpJZ<T
zx4?a%4i155flo50{~_=y&<EFntAO?b_<8Un;1swCd@J~7@SDu-KLj2GcY@o%0q|+&
z^*;<=2i8FoTnnxNj{*-d&;L{4d%$-9&HFzMd=>aS^ZQy0@MiFGa5K;zgMUIBydS77
zw8!8h{ithMZz#DwD{B7e8y)ukpVDUX3R2D;p5{4ATe#x|V;d(exxMVt!^!`DrG%ML
z*m}Y|Tu7KgYdS$eq6+AYtJH_Q#mAUZKU`ZsxkT)*wjYm^7}h^hk4JVPW%4Nz-(ez6
ztZwCm9&tI2YX0jVq##2nl}oZYG2-mc7O7z59YczcOeyCfvKPIx1T(O2e{lwh1blOh
z2|q3oJw8~-D&8Mv)GOu)@yAV9kp*`O84Rx$D9v|`*5ypcqRQvR$ycgQ;n}}WhNo&Q
zz8N?9miIPe*)yH+<li?lqC>V&H)W>i9}_VYVEmY}$L^pc9Azre_B7MZA+{!(kQhH~
z5w-8Pc+fV=c5Z+LvGgQ#w0XHUzEUt^&=!u_BOF7a;3S*0At=7H?B>&@v7?(xLOD*d
z2Xj1bfmQX(`7YX=oDgz2(FxTOGwdnqXf(N1Xp3ygI?hs0INE3;y+(<9+4(yKVt$!9
z9P%qsM_BVR+X-up>fb*HVqC{nfXgXuw6S~q4?kC1P;#?-jDFB{Z*gIWqQ(5yUe!Wm
z8Doro(bufM`CoJe>kj@G@nc#h8J=Xl%{)-ho97IoLdWE!HYAAc)-;1|ub1*s7AYI$
zkaAH5Tgapts#A#DAQ%10tD|3eKKhksWWTnSQ>acJ5MUXV@+oCg%4LhyS!`VJL_6HL
z5F@F`M!)j<=$Golm2fZAZm2<qTAo8aeA>s+-wTP`&pdVenI~^Q)fNb$&C};B9Ai2M
zR}>;83F#gX>*i_fCKbl0$i}K&CQ&8K6+M&}Lcj7Rvjh@vq+bKS{v6gDswwk)R+1pK
zs?&rl=Q-(Do|As%Iq8=%$Dm6sE<5|3vxk-ag&l2Ipc!dn`a-X}*inftyOV_niefF?
zo^FRw4kb{$k7;V<c6^H4I+qrA(T7I@kXp5iDt49|zQeDuV}5S*DlCXS+J;_v#I|xU
zO;y@W!h@=9Vm<fddqiwK=%}KUWn9PVh3Wp3@79yrtbpwhTy8l9s)U@9Wq;*(OFg=k
z*w3#_6cYo5Q4=00ZMbR!!VqVK@L_1bxYcO3=McsE|0tY|to{kavuXbSzhbXyzkJ#M
zw*{l~Q`q|-1^0tDgQGxm|DOQ&gXe>%f=^@HKMZ~cJOu6seb56_U?;c+ychfaSHU`{
zgB!vB!nXfi@IyfH{x^WDfb9Ht0@?ZVK(_wVz@x#}0G$W;%i!f;1uTQ>!I!Y{KMp<y
zejU69d^b1-o&!EFTOa7`fVTsk9dIvL1T*02K>mOaLW`dP-vKgkE0_ic!Ob9^E$~R~
z^X=!iDX>j}Z3_IOrvO`t>DZ>34vzSl4%=#+&u*#J&$Exr%t<!T^?yzx9D|y8pAG5p
zU^e{uEbe2wbL@PU6wO6lkRhL4G__3tm;E2*TYgF4n7w|qCH#8%S&KaG*`b%D7B~MG
z^B~%&Kc|w%(vm){+Z^*O0eK;Jq5#J}BX7J#;%$;=xUa8x+7>E|bQ`K~RnITqYm}49
z#&neFM2SM-Fo5ve-;R?o`3t0n>IBJcTfX{|P5`qslWzK4H#@;eVV$Lk9d5#AQzqu@
z36y2#ZLZaJrJNI`Q=Uktc+{M&2;rdEIll^JcEYxpQ!<*QnFy<=O*JK7g=g#U7Tl5w
zRE<<%^=kZ6YyKBJ52fc0`q)t`OSUjr_M1Su2^KKf(ON7{V5dSmqDh-LhvS;^ZTmvr
zI;?U&q)h-hWwM&qFs3f;%lXn>sH-{bo)urpDA&eMetC-OIh&`+=GhsIIUv7^e6%hc
z+pAN46)5Tt_D#hYHwP06K6FcqG`F6zibe#lwa&b;wX3#x-7XllwGsJ2cI}-yZd-IO
zvlp6LgWWT@JUi#9RM@^z)N$IGLrE8}Z&<KWespAo(FW>Yc4tpK|HR2VPRLR{+dhw1
z(6cDE_Vk&V(?@5fZ#i~EH*fE9mRkF$Z8lM*w5K~wTHW@wv$}A)gf93=TO~X8{WCD9
zHLYKrkf+00WcBkQ4RLi^oSi=cr^E+zsNniMmhk+_`fAThACaSc9s1b?zg#!2Cd*kZ
zElS4~i4C95btTOXGn|}=#+G*+imSb0EWkK+WphpX2JjgiEE?$Y_t8diokE;IjGf<U
zU3j@Ghx8~0>jhaAuK8OXP_*n11`A6PeOBxz<Y`49zE&Od8VCm?sR-a3!ShpSAw*EP
zS}2rl6r9A6zt5fpJx$t1VPRM2FVtDN9X6@iki*gw>}H)muVwI*%)+vVvIy)XcEA-<
z<Si=e`N?mL$=#eSEhT@q&|~a^GRiwdDo+*3F<hp!hpgY-gl%R*pSVy@#Vypr6Vujz
z*sN@*(1?_bOAjiPM<a9?ih13Sol2V)*x@+v2uY}Q>Fl?vKiSh!-A2Wazj@1Yr19kb
zu`Yjp-o|G-hc%oY=eAut=xqN*-y6^St+FgB+Yul=o?nVD7<2eDR9F}?X1@tHp_e8m
z)hB(<%C|iJ1-784h7KaRmjB{N(dubxJ96%>gs<b1pSlt{g0-_kF#K+pIyjf*aU5UW
zT-Q;2ZL+tssC6V)IxW;_=Qo<^+hHX(hql{qk5wu#$5t1Q4l)`kH#KkAuV(Dp4N*d^
zh)dnJ{5jb^BIU=s`8Jv(C_On8v!KckJMnB68ii9Fu=)QEbJG6~AAs!tnV_8h688Sj
zgP#FE2wn?LfNuwT!B>Ni1Yf{WzQ2Ht|JUF_Alv^aaNtj{^WOrr-(Lo%fDRn|AK3Z7
z10DnqfbRk`;Hlt=Kx_U#gRTD&@H3zbZUXWFd>C8*{ouXeSHWw+G}r?^i=F@5;C^rl
z>;cz+k7C#V4tN82A$T<SGi>?a0y+oaP2eR!_WgC>Dd5x0^M3%m1uOsuo(MhztwgVv
zg6{<{1AD+@!6%^Q&w)0$0sI;B`tJm<04IRX0k{r48T>JG{O<y<18)Y_QsJNNz@;$(
zD;5(J$2gM_VV}Y6z@@Zyml&e|e*%{x$Ez(R85xq|@hmMf?woeUWd?Qjvfpp=5x<a5
zrelGfyBvl!pNcZo)qG=QEy9cJ<#&&$#0)nSz0(Ur8+CIa;kqK)NS?W#7`Fn4vH@mo
zeJboBZl>n72i+cRE@(?P!woBg-B18r$X`X(8|*#bS=2$ukxCr9CkjO}1#OGLL&dr`
zT()gK;{0e(5Qawns7SJu3`<jG2stPHO@y$rX(VRmJy?IbtdCvvuSyl>{PbdIrB^(P
z&x|#-NIxgPQnekVbk%37RP%ZicPzDYb1QmfBr7cXie1+~C^|ST(6*Vel>WPt)e7ec
zp&V;@^SnQW7cE$0b=Kwh6FuAMiW7sPOriYJ&Hc7zwxtuVVT^?w)oxa6TcS6#(^K*#
z@Pt<Ov0rOmd%ambV>aZyS{-=M?psTu(!|YIWyrO3?xN+Nw?6(5QVa`R;RYmvc7BPB
zP>7f4c*Tz|O7Dy9&8G5hNS1!Em&9G@i+)oX-3Z&qC^XaQu#Jr#kg4hHsf~J*YVG?>
zU}2lx+~{dz@*#DH_p}?1ox5d}&n;_$r%cK9lg~%2J6=Jr^3M!qkuy78(i%E6Gwm|s
zX(*24(*Gz^>}%FrT5LY1_780rtVFS!9e8i2F^K1QnB3yR;ez#uI%{PpbkvY=;6ZxP
z;keD8_$5E7)HXo0O|8<Sr2ys8C}_DEwEIV~Z>#dzJ(5ZJF=zZPS5#%Mb=f^WN;JpE
zT3ZQ@7$T8G2!1b9N`jjj#USLKoBr2ch!cJsXmrpE$)M*eBNHRO0HIHe+u%HqEr^R!
zNry;?972ch;4I{w(yn02t+1V=c1Yd)AOvmQ&<pdv`MU%wBG$dht*a2TqHlewIY(Ph
zMOwFl(2mVAx;sHdZ;Ia0$*8xYWDM+Uq2>~{V`X#cI04Gz1Jl_agvW;jo9%cernWyI
zWXe6YP#k{DQL@1*<s=P@<ug&3QvfT@y3f$Y|DG^IhtZbBX?$cuk&0CxctH6pZkw87
zp5Y?#dwni3IIPU4T_*KZyyU&Z@`SpHOZ%=3d9_w2Vv@AR8d17Byx86eC$q3`v%hZs
z9X9(};RT(x6_^>m$9uz>D>fiW$_GaPV^!u)YPJoe2o<*y_x!2T_yjw4qBPyGAxE#B
zu_BhRu>F2(m1-RH{pK!hC8U#K?ke;wX&rab`E|mL*ewi#R<Bq#5-W(Mu#Xk5#60zS
z*f%I0SbI0_blYfz1XbpcXGJCRbu}uPtA*nx!Ul}2Iq*AY$D~=BuPWp_8Tt*eNrvIz
zc&*R5wD-E~fbEmgI}qE_xHGIL*jy{p)_GA7S=kE0p|N;TTcxk!@QkB=5I9vaH=8lr
zfg(2dfLp=)X*%6-%84G4Q>T}<PxpNnoz5~6QxWH=0(dQ^khAvivxi*zn5?l)3pIP8
zZs{u<g|VEzCR<f^#E#$p{~IyM+t{D7|8EcWzxMz8k3jqW?*Sjj#{X~Nwcs`20MOk3
zkAT;M+rX{hOW5|B>+gd$xDHH!k7LjO7<emq0hj?#20GX8ec1Hc*YB0!7BCI|0$ctA
z;3t9h@_P#SW9<01f>(oAf>(gO;EUMu?*{JzcLVL`|5R`_kbVCapxFL%;7Q=U*zi9N
z-T=;lXM;~+yT1i!@4f*z2d)9{$A*6ocr!Q(9C$Q%FZTO;z#Bmi+z37k4SyVnmMzh9
z<P#c72c=rbEBa->zrNEv?234Wvo-W{l)R3>Q6N?9UG#=C+(8uB)#Q=#-rL-jly+oF
z8#npj89Pfg9Ml?^#@5pirb{oLN}H(YsLF5U*a|$Bi=8GL(Z^kq<Jh7q6z^)kS$Ka6
zb4{ZV{O$JH0Vlc`Y?^R=r+a1|eU&zF$+O;Rd56+rFol%q9y&ZZ7Q|h@^LkM!Y7&JW
z5x2V|jLvTnPH8j|k@nm6H`sB|_70Ce*|aT=dRw95aeP#jC3o4g*>7XxTPo5gDH?ej
zdH-?TwgsWdWT-aaqpOeEZN1i#uU<mciZvA|pwa}&1qCU0Bd5`rgB6a4vvKV;mBEe$
zxt*GO8^>ESR`n2fE%OX(Mx;SfrUOAjMM&}#<`K$#A*{_dLl<qr#_55wnX~yr#l^wP
zY&z0d=8S7A3CYY*0+O-8zEJjf`z*dr-Jgg?a$NJ&>kPVRSdsUgbGI=BWHvIj!^vX4
z(@+Jj>V#O;mQiyhRH~b`bl`TKbJQUFQn%yxnHPC1+Zc?_SjrZ>OmkSjTj(htwFGVE
z)tFplOV2c$&o>bDlg7JY1&3N<!E485($@#D0|g&$0za^#>jaZatl+2NWW-dtVH1r0
z0APP!g|-{=kCaZT41RO<A<k`MZZf_brYWs$GF&h6r-w%MBTb1%M4fP&oH@>C`|IpE
zIKs`d9E__2sBOdF(bB|I;e6Y9S?AsFdT|-&ds~O=*)hOr#)Z~L;>4~^_^v-;fllm2
zT#o}9cC&G4P@>b5Cs_+L)tQ$?hR9UhubW<Air{41)-f>!-BbLv&iqM<htm{19V(*w
z$mu-o1qcPRjnK>NHJHhiCj@!vQ0zdHQ-wplO^#Phm+|>w2o6gJGPBUf+LD$Ls1a0Z
zUE9HuGm57~bi9G>7FxA`L+SD@n&LB&T=vu+=T~Z2DMs>*JDvtTuP5c#UW;uT)6~Ve
z+?^oBY}T&r$R|zYZ86Oes+kbv+s;Znd8pQE$~cg&<0sW!Rj!WR?itUpsp;Le53MTt
zNYC1!@f)3R;D+@c|2wBjU=M~Z&mKrT+-QL(lA6BO88mIuwzDQtxxk#xc~@JY!5E{p
zLtcxyTbI>(4OXsbK=rz_Nm2yBbknxi^V3S|FG`KxhESq4kwFqnk^TI<5({TL92H;h
zWZgO$;PD&u^QK0MO3+moVZtKUiW_yqcU|L|;)oxPW-qm#PpZ^-vuakZ6i>1oWlFJO
z(k|3|V|0l5r!S5@YCAuEd(c?)r*B*3igs01C+b|ESy0btH-nXupa@>jT;vpzDes!5
zoxp4+6zeUh#KV0p8WTDeC-knw4msOI#*dxJ&b*JEDT+P_Vx1LjEzJ_sm4W~z7-zX#
zYvIgg;PO(#o}QrD-0lgnK|ywiz^swRnzp${{wRgAprf!D+4c&LjwP8B@F(oR4uMA9
zQLmIDR0^Vhc$8r4@eomDF&rcLlfIp>HnKxMIdNE<&2~ncBi{`FKB|JnStycEhjUse
z&S^{2j2DelmPX-hdoGCxsbu2#P)JL*EW^B>?6;twRZ_;);@nuV*jBTiIKCuoN58n}
z$E9G?VWIceGRCFC2pCGu&iJSai@Gzmk!%nj2~iV;F3@B-d5X_@62&qWNtHk4tb=G6
z_S4C+qg1cds75F8WIhM2aW~l#Qk`Vr2k(}g<;@0b$Ry{G37b$aFWhDn9C1UW6R0*K
zA-!#U@Sdn>`q>bx<u8mfn>}B(e_?()@K=i0RD{jw1eXR;p(nL1t6E?-ytWC)A;KgN
z=t(rCJOCn-d9LDd-Z|IVv-jEj|32*0pO(Ff{eMTWS>J)p|5k7oXy5+{@O9wVu=^hb
z@&k0hbwG3f9|XS-z7J&J2JlDN{XYrr0juC9pmqL#jLrXg@H+5X&;oPd>EN4z`~j~A
z9dHCZ7RVQ%nEwaB3&1nMzXDf--@^y+Ch(o$9<TzI!C7zwd=5XrPk=K(zJbSpkKqUS
z2`~q~0sI|4fcJo(0P+i526upO0#|{*!55%C{@)0+=D!Y}4Yara+rgWF`~!cBAK+KP
z{a^t+0elJC{yF%4AUZz?zKoBAXZURDQ?8_^%$I~9bDYc)uG*!dds)g+(T5dO2w5*u
zP{Mu_wdR_Z;PeK_2E-1=xuiisknreQ#@4M~EMa-sR;tm0Qzmj(!JLPSa}fwSFH8%*
z^r(CJcf6nZAJi*t9U}J{XkQI88mZ7Ml$hJeMgoO`$r@DGQwP*O>)MncT7q1|;PI}J
zNHOi+!TZt9H;0VH0-1OX;YQKo9O~etzaWDIx8+Rx?%=e9M!{zpoR!?QP^@Va)K{3o
zDn2<hkrmU~N(y+s({>8pTt}4b7!Dwd^EPP+VT?4!ON}WO$ldp1Ak%G<KO?nE@`L)>
zo2s2$lf0>jI24ehc7Sd;FIs>5^KJHUp3ksXRt3P3nhJK%ij{K1{)lrrp`*C)3Fj%<
zSaAiXs%K?$tH!ta-ta)CN_;3k{_BzVQ`IXK9oib%bjEY3pXE<@hZ3|aoB<jVC^=jd
zv}ZK-=f39&m`O-)FZPg}+oPUftz{LA-6D?6QKGEWm{zy_0EUh%8g(mJI*Ef)4XEwV
z#FH<vF;w2k;d0L{)4sddOn{Ydq*wXpuFxIALnHkmOd%AGc@7#=lmzPkW$jD*2;(-p
z(C7?$*pHhA0voeH{4fc^F`a67`H6WmZvYcFQry-}+!VAqZ`DcQ_!XFNW{~m8@}XI4
zu0N`#EoW_MAqalFC`y;D6JjSuHL>;y2WAzHkTwB9YmvP4V|@z!Eo@c8LlwIf{u%zw
z<!ZqVIpbXj8=V5<b{D2nm16N-Sh~FUIFv2q%oplX$+)V-Tlo6&aDjA{yQMQ;cE_PW
zuR+|IC0Tei90UdVuM=NuiUczAudUIPmeIx(Hf4tQ)CI43iXw>zkCj6*`q4S4+(PdN
zgSY?ft4A*}Lyy{9mmM?Nic2sxOzLJ_EK2GPCR&SPB$Xl1k#_gWC)-<FpDbl!9ke{5
znx;~H`OEXQ{Vhz?8r5;si{v4kzSqY@t91#yz_kO(%{ynV7tibp4iCz9>IPvzFCGUM
zo8a8WrwrqE)l6eB`0`j8Ua?pl3yrZyV)PEdTZ-LbqS>CVr2Y~5#zt{3`*F-OdA~q}
zBw_lBSnD;=InEtQ>KfC^&01?=vDWirwV1JO^=tRj&SJhS76%}L1r^V~7f3L6j~7h_
zQ&xS{<U<i@BXN6vPMi>Yi{Yr)dpW-bUdc(9=FoAI++AiHUJb3PJgxu8z_HdGwol`9
zmC3j;$(~O|2dx$|S#ve|0|_^CJu6!Uf@5*vLGf0vgl3`OR<gWXA#GL8QQb$eQH8)2
z5i5?Pg^@a5DnuTRZ7vl8`Ro;O8$Gj&3;;-f4WLOQrR54mjl`$4;=>r9Q0j^CVlij|
zuDF&t^+LP?WjbUL?F<q2#z?n;Sdp5P2Q#&^pm{qR1&v8kzuGuDaa{jkzkMAlOY0lk
z(2H}D$@!HkV-ApbSi{((y_=liP;eZvYQSWpsi9sYM1;_mxo;`)kww52on{nBEgHu`
zc6L$sS6ofSyh7#p<)KvZ;b_rF?!?)=R4QOtHIV#PdB(bne=BBa1TVZXd!cULFAXiZ
KqTscW%KrtsZrURN

literal 0
HcmV?d00001

diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index a8eb69896..27a512a28 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -742,6 +742,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
   | EArray _ -> failwith "[Z3 encoding] EArray unsupported"
   | ELit l -> ctx, translate_lit ctx l
   | EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
+  | EApp { f = head; args = [] } -> failwith "[Z3 encoding] let in"
   | EApp { f = head; args } -> (
     match Marked.unmark head with
     | EOp { op; _ } -> translate_op ctx op args
@@ -758,6 +759,14 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
           args (ctx, [])
       in
       ctx, Expr.mk_app ctx.ctx_z3 fd z3_args
+    | EAbs { binder; _ } ->
+      let vars, body = Bindlib.unmbind binder in
+      if Array.length vars != 1 || List.length args != 1 then
+        failwith "[Z3 encoding] EAbs not supported beyond let_in"
+      else
+        let arg = List.hd args in
+        let expr = Bindlib.msubst binder [| Marked.unmark arg |] in
+        translate_expr ctx expr
     | _ ->
       failwith
         "[Z3 encoding] EApp node: Catala function calls should only include \

From 71ebd3a2c7970a0da8cfc0218a67d4d4ac35e255 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 12:49:14 +0900
Subject: [PATCH 2/7] Test for Z3 let_in

---
 tests/test_proof/good/let_in_condition.catala_en | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/test_proof/good/let_in_condition.catala_en

diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
new file mode 100644
index 000000000..a5b34deba
--- /dev/null
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content boolean
+
+scope A:
+  definition x under condition
+    let y equals true in
+    y 
+  consequence equals true
+```

From c711b0b1d7495920bd22c0d30e09dee347acc1a7 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 13:00:07 +0900
Subject: [PATCH 3/7] cleanup

---
 compiler/verification/.z3backend.real.ml.swp | Bin 53248 -> 0 bytes
 compiler/verification/z3backend.real.ml      |   1 -
 2 files changed, 1 deletion(-)
 delete mode 100644 compiler/verification/.z3backend.real.ml.swp

diff --git a/compiler/verification/.z3backend.real.ml.swp b/compiler/verification/.z3backend.real.ml.swp
deleted file mode 100644
index b079121a62b355df7eed65f529a5845f7c19f5a9..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 53248
zcmeI53zVf-Rp)Pr3W7|001hk|PbxxgCEe98z}TH;sPrQ#=tt;RfTB{lb?d9Do4$|A
zeROqoIv^l}0zP<UIZKU*FIIfaEF6dfIHN9cL{WnZIt~n=C^IswrGtPdIP?4O^Z35+
z-doibbPbNyP5yoBevk9mXP<rc-e;e47IvSTIqq(n+FRlC^_9wcePZ$O-%dU1i$7SY
zEOk4rm8^S7w>JAsueY*pqu$$jyjH)Z(>cF$y3w6#cIvfe`K_161b5xh>7L)!%~m_T
zUG-YO)~xNScUr5BX4c(xfuxoiTy1pPyDsfpsMXJB?Zv5XR%=eRh7v3%zx`{Q0^1bW
zhysKD($1S6U)i^J&u%?(-Nd!-o4)bvMo({F-=@Ge1-2=$O@VC+Y*S#H0^1bWroc7@
z{s~f`zxue!%c$3*Lfwvq@2iHs9~XY#9=?wc-T$ia`-S2AhllQ89ezJQe1CT6{#S?J
zcZTohh62QLd`-As58n?A-G5BDepmRuDpV-G|8?Q|9pSq+bpNs8`b_x#g`xY84%fda
zd_O8wD5n3l;reai`w2t$!{zO-Z3=8tV4DKl6xgP~HU+jRuuXw&3T#tgn*!Su*rvc&
zgaWn2N<}v8as9*mf3*MKeoduP1AD-3@bQ09seC_pDYy@u1Si0w!Mh$`skFh<z+=JJ
zg3n`ce-eBc{2usC@G5X8m;=Yav%u$YEPNDvAD9CUJd82^-QWy(9QYNC>j%Ip_*U>K
zjQzKR1@JB4FEP%46x<CCgTKOA@LS-gz$|zi_+1<f4}+J1DezGo7WacA;L+e0u-6;l
zI5-Brg#G`1@NV!H@CvX1Ccw4e1JLVd!5lE!sr4M6{jT0=_p^(Acd*jT`mVOPIDcv1
zg<98D+qG84{a(M@XfIE?>IHuE*H^Pemt9=#x^uPeRG-WJb$^{d>-~#)f|Hhhqu<j@
zZnnQZ=lUJjU&&IAH{38;sorpdn@yR{DSuwzp;m2mm3-Yo)?drAwwqOPxZhs1+lMR;
z!%@&iZK0XD*$Z}0mAcod9BYmKivE~i8no++S-t5FT9J>}R;S3sU2sc_x<6HV<~}R*
zP(|`OK_thg%B%a`Q4&5(!c)p&URn4mk0(^3ZY+<bq#p_$aeBShwJ;JlyR^7Dtzr_J
zkV_=ofJR2Y7w_}!-)Os<i>0VF-CAwksa;gf#dT;-Y)iAb?iL5)0(-UJt+jhiU({}P
z&!Ay<1~gm8t=4+J`65@<x}8CL(UO}Lr7!Jk)%x|7-e95E@6GLS;UY{nsM`fKaJWbs
zT(33S+;Fw77^k&5=x08;z$88YbRtPg64oeWun511dAVeTX|z@|k^4gC__LX{vNjLU
z5<6U@?;2K#Zno4R*G`-I*NNyMXMWVPDR;Kbo&KQBrRKU%FqC;NaW`qy+V13`TC3@5
z)V5pmElp$hJFBj<q}$LY>o(U#+Cw+qXeBF>7mB`k-wtDX)xW<2l?UxsXOWmA3e#VK
zy2~q_L4UYmrrep8%#y27jK~T7tlLs6y?CG9cO=pb)E58Esos&sbUdqluV3r-L(^Mt
zCE-*@wKDBP7R{y=!Se$}YluQLwRoExvv$3+m{F2*ha7=a-K+<_X-MDSoIajjG<LR}
zb=}%ZqrO72@MBN6mW}>hGJ$HlUEolAF=x$2mwX%jMy=Vn6dIFKaE(gPZaeh0Csi|R
zFC!m(Bh<Rx+Iq#(a@8B$v}-ncecdZCAWay_99iMT`%DmKy&jc>1oir$HK1P@e|lao
zCa~WfL2OQ$>{JE^e2%+a=DDxu+gWTqpc06-<{<MGwL-1ds9qp=?20OaD9i7j3Y=aR
ztM3R@Uv$O;{Q+#wLuBg<XSwWmr{UzO9{;!-@)Cx^)gg8_V*tqLCraE`h^`7*qbR20
z(4f=p6$*>=b_$=1oag(ulMFXG;nV8E2dka7iVsgZ6=H{f%{Tv=SlAaf2nfV(Uf$Ct
zG)|D_l%#s3DC{<xeAXVc)I?TNCz<A{QfkCaD$vhbtDSDGyPk#|+G{y$ONhYkYby*<
zspnFi8Uq+|PO@P{>`@6u%{Y+m$f-V=MyObqNC!$>Xo*5ANXXE@TWA7Nz(gKBa;xo-
zN}t4MsR53V<Ouoe2z&%hcCjY8YJE46DR$d5Y|~Kdxj;a$_7X7}OklnK`p#9xm%jJ|
zxtBG2p4K&rX5Auj8XTf-umc_~@|B4@*IREbbeg{2hyl+betb-I)PPZL8n5HfFKDev
z2fL9$k<$u;Hu(-zc9OR7Vli84v^93rvoyRS$l9vMJp+P9=?6xQawWo$9S7vlP}PFS
z6x&Af^(MVEPdS9T#KEv!n;qjcmJyDF==DaAVJ(oKFOfeKOwua~yjc7*$b|wWOh!qe
zwEnN27~Wm&c9y%fmKw-L4fXo+FcFHc#3;JH=IK0=MNmoEKs>!n>N&Z+I1VlByTeE+
zeHSE6M!t~1fr`3dOb+Gn-bw`q8^E%sVBiM2@4@)jJi)=O=2W;IA4~i|y5fq{UgxxA
z&%@RS1IJ9ETiXN2Yv(gp^{-7<I;)5b)G+&=?)Cj2hY?M6|L5ry#{9+kTD;}SI6vq&
znmtqAMB8JHde-itlK8F_emV_%y4_o)HHlAl&02eTP+QL2a)*%RwrGz6)M~`R3n9{M
zv>ILql9GX50^Qvm)2B{NpExsf<g`0^${jj+;_%FwnUg2@b<|Ctc#(Vl%!$JcG$`8)
z+JWv)V=kQ^6=lku&TQmRT8oT&-Nu46IG=$PF&3FYzW4xA3XwN4ecH{Oo^ZEJpPo6r
z!`(4+=C+e(&nU68?Iw(f?2rOVf(z>oi=m0SDs!M&TT>}&s13eT((~53s0Quj9gH(e
z{WWN7L|p0jSNHGQwYIi4Ra>pqSF)*2cX=1-h^)O`$7T*4IdS^P&b?E_p^|NZ=C0P)
z6}mlFDg6=w;gF!7t)f7-;Vh9rdPm@kVr#vqGhl#Ncbx_4PmC7z&MLn&IL9U}(rDUB
z7VqqE=d!Mp4o9gNN=SGjP;p}NfLjk~w>y0+a)@_#M?-wPySe5g;HP4M`*Ry@%qV_7
zNBL_&>2>O8QRske<QOKL*9yHl*QJm2rraS)+-)qc^j-DPq}#iD?_M{fWPJa&cJ6fd
zqcYNSBX#&*MV*YQN)QZ6T*34xK#5^}R*7qkpKBK@vi~u|D`$fJ|9si8d>+E)?}8)X
zYrsR;`Au*$*bDZ6k7MUQ489k<4BP>}4SY5D5Q)AOoB_`Tj|U&Zw*Me_75Fw#1z*Cx
z{|)eJa3^>&_z*V!uYs3>z2Iv7#?F5)7=UMh4`S#4XYg{c44wkshn;^vI0v2xo&es5
zt-lU-2Als4*!qWp&Hu%#vGKu=g4;m_d>GsQZD0kQ1Uo?$Tn|14jXnf^1H1<GfarD_
z6hAaMAC2XQ%-}NZ&NQl}PSe|3@(dtDceqRYkjM;^-VXMc_0wKYssKYDP6BCMykrKp
zWV!vJs~QI@&RupVIt-CJ#dMcZ>yWtm<uj7zXByOK%JUsMSSj^O`*Qt6cE8x(vT*j9
zHI;EW>(4h(mAcCqq4RP_cq><r@C3Q%w<`7?|AcYJWO~rAc?w0U%?K3rJuhKu8l9xV
z22pHD%$_#IW2$w2Ua}9V8!2*WU+}Qp=_an-Jux|#^5n&dYbTO=9WA1=(c>kN^tjlW
z7}v<ctLA7SNpnOhvLYoP4d~W&Mi#75FX646)bozawIwWTrgWqcBvyA!Hapy!h_=vx
z5Gcm0jr#diiRxw*SFt1U4+q0sBq~&49+?w(2TJJ$OS)>@5p$9G7Fq*=G;@86VWl^~
zP+s$P9^xif2F>n>3aCpqUP{32r0UV~Q#;OM|D)E0X77pA!E8hYlhD<}u_%S2ml6`^
zkcb(ctpR4`LTa$l6k}r5RE_n?Qfgj}E!Ijb71Y_hCcelqH5GNZcqn<D<#yu|gSHum
zK|ju^RY*4x-!a%pFOW4Yn@z3~6t2(${E_Xq(nd}n*27hhz_C`g(78q$o_>@RV49F|
zjD7{LVY4lEFtW{cFlFPJYpvTDN6Q2WMR9!pMku8YN_Srs=eX+eTK7C^2~HILK(C*S
zf<g&c;iRh-pQ#Q@MiV5sH|+8BK6YMkq~72XPan$rr1Z|zKP5h`#OBo~@_ll<4(Gb5
ztJUo%LCAT?(xXj+rkpYy+puZ)%?mbLpNrxvuTE}pAFN0@ka(Z(bmzV1J#V6T*kxL^
ztN1*kiAecXNaR*D&rOd{xvAu0x{;!5=+98hq8U-7BaA+)jBq5H87${<!}rNhIo*v`
zuYVLlu>?=K-hebsUS}8S$UV27A=7cZqzsf6dL=3hKI$=*#wppCUqCMIPT5Zqhk|i*
z7sFn5XQtch8ts;9ji&jkCuVsmdUNLdeH(X-{|BqMA5fepjE1oC4mXWHyVA<~jr!D#
z_nO%-qY)?<o%T3XKikBl@$O2KU2#N1$2Rwu>)}Sk8CYx5)ztJ-OVz!jcPcg%Ty~Te
zX?NCw_?MB3wHQlosaL%`Y1Aj9$dsrKSxtrd%j@Rm<M@AOy4&rn+3!tgV$Y1H3M4(b
zYW_y0xp5ldp$!ue$9hF%Op}`s(NIKgXUw6td1n5Z4f8r}1GbktDs#DG`QB?;1{qAQ
z$Kc6+Qj<y&ZoVn*MaroMc;%^Ywns&>29ZA`5J&oKA4|54k-8{(Nq;Sfw4w~K{!q$!
zPTW7};suqAFEM}g?}ct3x}{NMwvVu3ME2x7JP6Yt5MryW4Ly*xrZsN$73bXZ;KV&U
z+@5dW9ds&qTFGcELkBfiH9bLUsyU+>zsL1s2cs-7fWq2~@>2I2*m}M$$5CvpcW<>+
zROA${>2lRi*&<>z$B{10<8=9<$2S!Mym3}uWpNo=NG>4c1@?tzEp$`&^_|t)<Auox
zTb200IB+am(cro%rYf=$ts&<c^LK$4MtMuGZNgv4fm~)VUPA0Qy>cMyqemr6pXzbB
z6Q_<c11HLLaUgf1lD;%K8THfjj<l7Nhfm_`(R*rj8>*6~5(FsvUD0oeLY?cJF|F#M
zW@Ac1pZwNw8q7|gI6ZSl?wB^q#@A7FI%{)o;_1B!SG@(9&}=MBNdnB1>4h;R+cdca
zrV&D76FYZ4XJV*g2y@zWYRTMuOKz#vSH_P2_w$b*ZeqDjXSuKgAsu~N@_R{Y1^3&$
zX;3+HnM<``iCIDtMt*$okCT=+l5+Z2)hdT&GfLUAL>EodlKp=Z#_NBO4a@w0jNg9;
zHh&N715;opxCVR%yZ@u$0k8u0gMDBEd?WZgw*N1JH-Hv64UU25gQtKegD>C<_;v6Q
z_$e?8X2911#R9ww+y^d$=qLD>{QZCM4SWE+0=xh`56pls;ve{F@DgwgJOO+JAHkc!
zo4~E$bNC0|2Ij!iz=!b-yaPM{z7w1T`@z?Pzr<JY9`IeD2j;-z!Jpzcct3b0I0&u-
zUj=^eYU&H7!8d@b!H4h{ycM*;i@+i98EE{QK(zjO(fiB%B<@LO{t{xQQn*aly4}3Y
z6V}xG{oL0}+7n~?j;TpD6EL^mO($14mI3lxs?ti0xhm-z%t_(IlC#kUq$ZBjPJ4)<
zqxMxSP0=rr3YmKUEzC(E^qGdFTcWShCC&R+ui*zQcXcl-y_gXnOH|BjOzE!rxeUj|
zk=zw27gOTJ_c0WJiBxIxNyrp4U@pWP#f8^Nz&f(#*(IjtZMxBP0#vk7(ZTbZ3XexD
zi>{R56{L}qa=D2-f+vd9N*q;1D#@5D^ObG~ACs#N$vxjVC}1>Vlw#&tDvG8dNjBVA
z-iRx{@JM7?q1lS=uWGS^|4e#@nOs}w8i!;<*U)@MdRt>DpWRYlt6>}wwZcHPTRN%y
zjrOV1m28k(Ebz)pS6AnI+3Nmuvnoy+%Zg$6tOhpaMc?0oFDP8D^}=vE@${M)RzsdC
zA(SVV2mXrnQ+XlukWb8C8quTt<)DB}*)Qo+m<bX@-X$B=G0hHCv#I5&9hw<QSIxj)
zl*){{gpiapBHUs!#r)*6{nE;c({p(MM4EntvM8-<Xv)nFN@X61L6yzW&r`!JXbnYl
zA(iu#WWER6AYBXr5gkj78FrNO;&wZ-P8ONcfhSCHH#-?8LQk<VKEOqWtfnFroMX`~
zOx7$7n%<%>(0Z;k*%|yNM&Nv&F}t|Zz|~2vHowhGk4<pfR2<s%SaaTzV4S+WFq0hy
z4Lv``vL9ifYVbK8L>rq#A3UNUl3Y^?epKWHZ+ffT%yHRag&-H%+SoHaKkh`ORK?z^
z6~0MTa3FNnf}gJFry%)_E%Hs$!@qBhx)t)Er&f(HON(Al+-Ur(_TVsyjY*eXKk4m)
zf@V76<<pq3fM!c`;RM0dvx$%5AmYc4DJCFssi*9>>O5o`rEFxV31?n-{0I}@o%Z$p
zV8GLjeg6*O0_s?dv65oQ2d2#C3xnP<{8*-rSM-qNiOI=)vL@97IV3;F35*Iq(<2?e
zq`XTwm1k^HqOq=98|;?6<{nE#=p=cIiIYmCtnj#m)=;st>v_m(v$7ai-V1fLMRK`H
zCxgv>pj1KK3zncN>(wVL^JUDe<f%3-3hopMqVvUS7u7*m(lW>N-a%W$!tC*Ji=#c6
z)N}ukrR{vUT~9V<xG?06uEJ5w-&mulx{|(Dyr8#@$Of4IURi4QO?ZA5=`5ztGJ%97
zNY&+ft|O=?_|M-Kt*s2D9uOM^I*H7okZ_wX*HJ|a8n>i=(aRrld^YNPjKpQ#bEGCa
zcP5L|RgE!}nK9&2JI}=P{ZiX2dtvTSIUBDq!0fH)S5Aj8DyC`<_0D3&62)VNN~K(s
z>QY<&3u`4$4RdJpiUY9T(uAmg%Gxrjmm732UZ>UNZKCk-jeoPims~q0ub+98qPn5q
zJRfX~(u@TUnx@L_P;pWyy4Oa?4-d(Owc+rh_k*9Uy)dsw=NW=bkEo(T;FpM=lhN_X
zx1Rc{c~6M&BF<xJi69g-2J^bXo)?(YF`2)ZX|~eFNCN6Kh{eE_e=X}u_CKa=<=@I4
z#r}`$?>~aA|6}0QU==jL9YFqoM}bdb>wgS91l|cU@Fehl?0eb&F9nO>M(`w{bpa1!
z-+vDnfF+>VfTw}aVB5bB{0jI{@NYmJXe~emd=eY~W8gv121mgz@YmS+iWB(v;6Bg*
z3!ny`1pXYm|9^rX2HywHf}`Nuz^Cy6JOI8Q90fOluLFO8{r_LUD}j6hyTE^kK)(&X
z6Wjxy3BDOT2K*xS|J%SCxB#vPe}w)2y&wZm1pgb`|Chmo;D^9vPzT4r)!=WS{kwtM
z;0M$W`Z)WD`K{9)WTvn|oSPq$FGM~JgHnhj=<lVUMAbCgaE@+o68MRqm6;#xh)|es
zW=s8fI{&z|qF@-B)a&nwLPbSJJG9V-{+=K&;CDYAQSIX>?o)zbSZ>zcO4ep2nWhYQ
z*b<h-lA<Ym66aVw5#@rJofnc%R>r;!iOJlIYAhN;^o!{sTXR5(RfVCcgOtXI5pl&;
z9DbHA5A0_&_0D}qWI(o-&k1-6s-)3dQJhF4G=O4z*`|54Fh8e1!}uI(rOEMu_s)*>
zvPW|uF7dEgso*nSpDWGgsn!xBV`uClNj9Igi%AqC8a;Q9cjco&$j?0ANX>U?pYuU8
zVp3)q<HTJEspeXFrf<JXqB%INHNT%CB-b;ArJ~!nxVGZ8?3YxOGzvwSJFMsj7Vx^e
z`8n9TmoK}P|0`L(Vv+S7j^InFUm=ij3WLq!tR&1WpLw5&NqC+NBhs-{z+g0AcE@Zu
zFwTAibg4?-D>KFnw-|ch@J!4R&A(^>sM+vf@d?RLg)&3Iy&5BEgpr9D&GJAOiW=uV
z%m7F+C1KvfZ7|m~wq1!EY8kCXPW>p*GFZ~FcGXB@D4MP7DglKI@~t4uD3_lkYDLk4
z`b2M`;u=ktnjI9jln9-S+1sX)@prHttRMyA$JwG-@?rpuCxm90x-q-Ln={@Cpb4M&
za*3T&F^1}BiWwE*eb@Hs^6Ll_;_F8+36)i1(IKWUJ(k#hjKK$2FPH<TI4y<3gmg(w
z$s9FGMPb@%iCOI81HSq;zqR1Y>4h-Mo#cL1Yv#icr5Rqy=BkQE=7!uYX1kbM)!S9G
zT=(;sLvvSl-HXmNFRJ%^{Irj|;TegK5w`Xs$FGYEGPEa-3xCG}%l|C0WO(3U9)qIL
zGet8M`N8%4z&tA^w$L;*P#h#}pKs6_9UtY%+X{uUY;>)f236C?FRGm_fbQa?o;MRi
z0=i%w#LH3+3JHaYA72FZ`9h<na?Pi75IVMqYtvY<!h2TY*jHmU!w|2_g-7Yh6Rq=v
z-Q5{!6NnIAk3`_PRC}AqG_zr`T<@svgm-g-#J9WIh4LH3nk6NvKz(}?4~Mn)>|E4Y
z)ChKI$;QF``<?xf=%o9~yYS3b6s<fMN(oro&dciX*@rBA|Iq`d3wDsHGUK8}^SWCV
zeU~ZJaAVuj*S%Qf%dpwT;grQEw_@g1H4n~2Z$)*{$0}Tynu_gQ(amC08WR`TD74ae
zn=kKn(v-}j;`?YY_<Yi#KaRwnc^aD)ne0<meHa1L+y(^<69_$ZMQe3+GB4x`Nt6`M
zykM91#S)FtIE~50{Zv>w+>oN_-y9W~nm#V%EXhfU3PEz7?g{`-Y9b>>zjoe+enR~;
zum{R2L@~yBrbw?`leC0GL1uepmC#DQsa`5?FM5dy7C#=0i}&)$N8Ry}2YeA$Z!4?K
zDP{j467AcXEBvsU6nls9V2~CHye@F-5Rc23Rpt|=p4hu6Iz^MxaA4U64!1ImbW;oZ
z-cSs2*CB+;1uTdl-9H$X(3XN7bprtd38Kh^MSMpLw|t(KvLuh}e@xuU&&lq@{;$jS
z<nu0U{MUme@IvrBZ~%N78~<VOULd=F8E7AX<KXGw6WIBG0^<DtIsSeg_&e<UKL@`L
z-U%*)+rcxzUtr_^68Hgd5%fR?t^<z&SA)O8-hVszS?~b31DpakgPq_{vG?BzejNM|
zco8@Vc7w+N#REJHz5}d-8^Fh~_dfuB61)+-7TgAQfNufXN8sJyjo=9Q9QOX(z^lMT
za4UEcxCVRzyZ?8=Z-7^W^WaXf5B$y5+ygHMd%>S#^D92!ec%VcGPnyo3uu3Vr+`18
zJ>(NmyJ(*Q|50N)N1%N^XwbSxj!DDvTH~Y~*tum?Ju<zzicfP1b~$oVf3Z^fpu08e
zzX&tv0D&j>@xlQ~1NqoyvpsWmB_%Oiku0pbTd_0HRt3L2+j?0+=Vj<$wgJ*4GB#Vb
z$7SAoSnPjAgT-4fDCaVjTzk^p=z=pW_R2!~=){^>+eoLTn7)5x_(1FjzfFzJXZUB^
zgthuGekN`#XpIr;Mz`<T&oXbFEIyv`E^Z>WR*7J(F(XiX@|iJhM5qKRuDcOkQ&lH}
z(h6%m+pK9$j~6V&A+yviIed967Fg3fY+6ulG#N3@hEm3xJ*8KDh#fCCye=rw)22P6
z%|xq-c+r-U^=BE|bKd{R(^S9F!}(KN4K1P?wv9YS$$ig$X7NSi018ypgiMW>^ie^5
z9$zVby&}6Zfk8?C5wYtSZX0IdaV#XBePnzcdAPtfvYxKM&pixg7M00$;-~1~RdXqS
zSv)+NT43g!G5=XJ@Ublj+~x)X*ReEI)6===BZzX5Rh{)df#u0Ew~*YM>8IB6L=PB0
zNL?Igg3qp^@_0{BY-HqXE|pAe6Wc5`Si~|c+a#RANF#Z0Gvk3RyHD=PBq6pg=UvI=
zH9Ug&aYIrq4FmeIMM<?)sri+WXvb{u%?Drxjni6;EN6#8<(BA|k=j}STI)7?isT4P
z5M7(Yek0r^Z7nuq)il0K(g=%w<@Oyn3wso!Q~|5zzxM`FXB8Vl3PiAWLbH-k)I80j
zkvze(wF7QpPL>rrf-qLp@JL;@BweG~oTnn139g!|tu`T{z0zP{!7C?SO7{w>?kT5g
zY+^-<gMw<6<dNMDijtWTTFp6bt|SeD_OKN>RHK|9niU3kT9iI@MDxXi_Cn`k)PLy6
z)w6B+Bo<NKI4%p3czdTe)$Yve$9=`;qIEqcMRRJXFvaJGGtRV!4*N>YT_MYuMs*|s
z+R2DTp@;9OO>ve&LL;p#_n1!EdGBVL&7FY*#<3(Z)D{4i;u_DV(6GqiltJV!v67ev
z{xf!?lGZR`1}e;&h#jko+ALs)J3pCs2QIS=(wekMG>9IHZxpt72|A|{`uvnRK+DTR
z$kf~Gvz^tsIAKFEZ1EjiE~!Lgot}DpW1nX(icMhqm0-ml%nEoWZ``SDwONY`=V!59
zv);VwI%R)O71h2uzaNO1_(~M{VdN}oh6T;Ca5+v|!nLWdiz0;xd28%AAu(5M>~n_@
zBKdp8It)c3yRox1zN-iRqXcq&6Pd<%N7P5g97kB`#Vs!a^HNOb*)C+NvSm(}Tai+v
zussE%X<CgaKmAmI-UfvTVQZlrUZTX=E0K{a^kMJ1U?R>>?p_$N*~^cLn(8uXkF_WV
zJ*Qg)(9t-Ni6N%vZ7#Fql<;}s7-3dc|L#>Pvj5LxgKLjI+5d5W`;TGke-Qi{xCmYV
zZUmpj#(xL62kZo2!nS`Ocr$nnxEtIBCc#y}(v9Zp_V+dgwkfbpfo%$GQ(&6{+Z5QQ
zz%~W8DX>j}e^?60!i%43A&5y9VRS$+KZOa@Sc*;vJzsd#Z?;#Q(67W4ukf5t*6b_h
zPV$L3&7<j4$V8L>d3h?jTiA^$Sb!ErYqKxor&;FhUT}*Q-?6Ei4c@VPW8Pr`XoEL2
zHRPvra3+}L9QNqL60R~c$cqP`;|N8h(vxo2OW1V>Y8P&(m@JADy)U~XGfQW9@Q8xS
z*j$`dXXLAg4><P5B@|7+loY>x=$S59P4DxLN76XVtpOhJP4^2)PiX_F7&z+7aB}qu
zukyg?ThqN>M(Bp^kdYke`J&*$`r+ukvRKpP53x{}VTVZcyU#hBu5Gi>cz;~Hm)^u(
z!(OdnQv_R*#`YM^0h>T?;ED)7TJaTY2g4rYkP$DVxgqq2+5fxfe_EF=`~R-c7yl4j
z|7XEl!0liLd;xp^=fIDEKDZk!fNud;gU?~_|2FtB@crPq;M>77z-RF<XwCmG1I_>6
z4_*ge1fBt&0=~dJ{~v*001dDJZUbM`{66?Y@Sng%puGa03a$d0_t%`i*8cAWpJZ<T
zx4?a%4i155flo50{~_=y&<EFntAO?b_<8Un;1swCd@J~7@SDu-KLj2GcY@o%0q|+&
z^*;<=2i8FoTnnxNj{*-d&;L{4d%$-9&HFzMd=>aS^ZQy0@MiFGa5K;zgMUIBydS77
zw8!8h{ithMZz#DwD{B7e8y)ukpVDUX3R2D;p5{4ATe#x|V;d(exxMVt!^!`DrG%ML
z*m}Y|Tu7KgYdS$eq6+AYtJH_Q#mAUZKU`ZsxkT)*wjYm^7}h^hk4JVPW%4Nz-(ez6
ztZwCm9&tI2YX0jVq##2nl}oZYG2-mc7O7z59YczcOeyCfvKPIx1T(O2e{lwh1blOh
z2|q3oJw8~-D&8Mv)GOu)@yAV9kp*`O84Rx$D9v|`*5ypcqRQvR$ycgQ;n}}WhNo&Q
zz8N?9miIPe*)yH+<li?lqC>V&H)W>i9}_VYVEmY}$L^pc9Azre_B7MZA+{!(kQhH~
z5w-8Pc+fV=c5Z+LvGgQ#w0XHUzEUt^&=!u_BOF7a;3S*0At=7H?B>&@v7?(xLOD*d
z2Xj1bfmQX(`7YX=oDgz2(FxTOGwdnqXf(N1Xp3ygI?hs0INE3;y+(<9+4(yKVt$!9
z9P%qsM_BVR+X-up>fb*HVqC{nfXgXuw6S~q4?kC1P;#?-jDFB{Z*gIWqQ(5yUe!Wm
z8Doro(bufM`CoJe>kj@G@nc#h8J=Xl%{)-ho97IoLdWE!HYAAc)-;1|ub1*s7AYI$
zkaAH5Tgapts#A#DAQ%10tD|3eKKhksWWTnSQ>acJ5MUXV@+oCg%4LhyS!`VJL_6HL
z5F@F`M!)j<=$Golm2fZAZm2<qTAo8aeA>s+-wTP`&pdVenI~^Q)fNb$&C};B9Ai2M
zR}>;83F#gX>*i_fCKbl0$i}K&CQ&8K6+M&}Lcj7Rvjh@vq+bKS{v6gDswwk)R+1pK
zs?&rl=Q-(Do|As%Iq8=%$Dm6sE<5|3vxk-ag&l2Ipc!dn`a-X}*inftyOV_niefF?
zo^FRw4kb{$k7;V<c6^H4I+qrA(T7I@kXp5iDt49|zQeDuV}5S*DlCXS+J;_v#I|xU
zO;y@W!h@=9Vm<fddqiwK=%}KUWn9PVh3Wp3@79yrtbpwhTy8l9s)U@9Wq;*(OFg=k
z*w3#_6cYo5Q4=00ZMbR!!VqVK@L_1bxYcO3=McsE|0tY|to{kavuXbSzhbXyzkJ#M
zw*{l~Q`q|-1^0tDgQGxm|DOQ&gXe>%f=^@HKMZ~cJOu6seb56_U?;c+ychfaSHU`{
zgB!vB!nXfi@IyfH{x^WDfb9Ht0@?ZVK(_wVz@x#}0G$W;%i!f;1uTQ>!I!Y{KMp<y
zejU69d^b1-o&!EFTOa7`fVTsk9dIvL1T*02K>mOaLW`dP-vKgkE0_ic!Ob9^E$~R~
z^X=!iDX>j}Z3_IOrvO`t>DZ>34vzSl4%=#+&u*#J&$Exr%t<!T^?yzx9D|y8pAG5p
zU^e{uEbe2wbL@PU6wO6lkRhL4G__3tm;E2*TYgF4n7w|qCH#8%S&KaG*`b%D7B~MG
z^B~%&Kc|w%(vm){+Z^*O0eK;Jq5#J}BX7J#;%$;=xUa8x+7>E|bQ`K~RnITqYm}49
z#&neFM2SM-Fo5ve-;R?o`3t0n>IBJcTfX{|P5`qslWzK4H#@;eVV$Lk9d5#AQzqu@
z36y2#ZLZaJrJNI`Q=Uktc+{M&2;rdEIll^JcEYxpQ!<*QnFy<=O*JK7g=g#U7Tl5w
zRE<<%^=kZ6YyKBJ52fc0`q)t`OSUjr_M1Su2^KKf(ON7{V5dSmqDh-LhvS;^ZTmvr
zI;?U&q)h-hWwM&qFs3f;%lXn>sH-{bo)urpDA&eMetC-OIh&`+=GhsIIUv7^e6%hc
z+pAN46)5Tt_D#hYHwP06K6FcqG`F6zibe#lwa&b;wX3#x-7XllwGsJ2cI}-yZd-IO
zvlp6LgWWT@JUi#9RM@^z)N$IGLrE8}Z&<KWespAo(FW>Yc4tpK|HR2VPRLR{+dhw1
z(6cDE_Vk&V(?@5fZ#i~EH*fE9mRkF$Z8lM*w5K~wTHW@wv$}A)gf93=TO~X8{WCD9
zHLYKrkf+00WcBkQ4RLi^oSi=cr^E+zsNniMmhk+_`fAThACaSc9s1b?zg#!2Cd*kZ
zElS4~i4C95btTOXGn|}=#+G*+imSb0EWkK+WphpX2JjgiEE?$Y_t8diokE;IjGf<U
zU3j@Ghx8~0>jhaAuK8OXP_*n11`A6PeOBxz<Y`49zE&Od8VCm?sR-a3!ShpSAw*EP
zS}2rl6r9A6zt5fpJx$t1VPRM2FVtDN9X6@iki*gw>}H)muVwI*%)+vVvIy)XcEA-<
z<Si=e`N?mL$=#eSEhT@q&|~a^GRiwdDo+*3F<hp!hpgY-gl%R*pSVy@#Vypr6Vujz
z*sN@*(1?_bOAjiPM<a9?ih13Sol2V)*x@+v2uY}Q>Fl?vKiSh!-A2Wazj@1Yr19kb
zu`Yjp-o|G-hc%oY=eAut=xqN*-y6^St+FgB+Yul=o?nVD7<2eDR9F}?X1@tHp_e8m
z)hB(<%C|iJ1-784h7KaRmjB{N(dubxJ96%>gs<b1pSlt{g0-_kF#K+pIyjf*aU5UW
zT-Q;2ZL+tssC6V)IxW;_=Qo<^+hHX(hql{qk5wu#$5t1Q4l)`kH#KkAuV(Dp4N*d^
zh)dnJ{5jb^BIU=s`8Jv(C_On8v!KckJMnB68ii9Fu=)QEbJG6~AAs!tnV_8h688Sj
zgP#FE2wn?LfNuwT!B>Ni1Yf{WzQ2Ht|JUF_Alv^aaNtj{^WOrr-(Lo%fDRn|AK3Z7
z10DnqfbRk`;Hlt=Kx_U#gRTD&@H3zbZUXWFd>C8*{ouXeSHWw+G}r?^i=F@5;C^rl
z>;cz+k7C#V4tN82A$T<SGi>?a0y+oaP2eR!_WgC>Dd5x0^M3%m1uOsuo(MhztwgVv
zg6{<{1AD+@!6%^Q&w)0$0sI;B`tJm<04IRX0k{r48T>JG{O<y<18)Y_QsJNNz@;$(
zD;5(J$2gM_VV}Y6z@@Zyml&e|e*%{x$Ez(R85xq|@hmMf?woeUWd?Qjvfpp=5x<a5
zrelGfyBvl!pNcZo)qG=QEy9cJ<#&&$#0)nSz0(Ur8+CIa;kqK)NS?W#7`Fn4vH@mo
zeJboBZl>n72i+cRE@(?P!woBg-B18r$X`X(8|*#bS=2$ukxCr9CkjO}1#OGLL&dr`
zT()gK;{0e(5Qawns7SJu3`<jG2stPHO@y$rX(VRmJy?IbtdCvvuSyl>{PbdIrB^(P
z&x|#-NIxgPQnekVbk%37RP%ZicPzDYb1QmfBr7cXie1+~C^|ST(6*Vel>WPt)e7ec
zp&V;@^SnQW7cE$0b=Kwh6FuAMiW7sPOriYJ&Hc7zwxtuVVT^?w)oxa6TcS6#(^K*#
z@Pt<Ov0rOmd%ambV>aZyS{-=M?psTu(!|YIWyrO3?xN+Nw?6(5QVa`R;RYmvc7BPB
zP>7f4c*Tz|O7Dy9&8G5hNS1!Em&9G@i+)oX-3Z&qC^XaQu#Jr#kg4hHsf~J*YVG?>
zU}2lx+~{dz@*#DH_p}?1ox5d}&n;_$r%cK9lg~%2J6=Jr^3M!qkuy78(i%E6Gwm|s
zX(*24(*Gz^>}%FrT5LY1_780rtVFS!9e8i2F^K1QnB3yR;ez#uI%{PpbkvY=;6ZxP
z;keD8_$5E7)HXo0O|8<Sr2ys8C}_DEwEIV~Z>#dzJ(5ZJF=zZPS5#%Mb=f^WN;JpE
zT3ZQ@7$T8G2!1b9N`jjj#USLKoBr2ch!cJsXmrpE$)M*eBNHRO0HIHe+u%HqEr^R!
zNry;?972ch;4I{w(yn02t+1V=c1Yd)AOvmQ&<pdv`MU%wBG$dht*a2TqHlewIY(Ph
zMOwFl(2mVAx;sHdZ;Ia0$*8xYWDM+Uq2>~{V`X#cI04Gz1Jl_agvW;jo9%cernWyI
zWXe6YP#k{DQL@1*<s=P@<ug&3QvfT@y3f$Y|DG^IhtZbBX?$cuk&0CxctH6pZkw87
zp5Y?#dwni3IIPU4T_*KZyyU&Z@`SpHOZ%=3d9_w2Vv@AR8d17Byx86eC$q3`v%hZs
z9X9(};RT(x6_^>m$9uz>D>fiW$_GaPV^!u)YPJoe2o<*y_x!2T_yjw4qBPyGAxE#B
zu_BhRu>F2(m1-RH{pK!hC8U#K?ke;wX&rab`E|mL*ewi#R<Bq#5-W(Mu#Xk5#60zS
z*f%I0SbI0_blYfz1XbpcXGJCRbu}uPtA*nx!Ul}2Iq*AY$D~=BuPWp_8Tt*eNrvIz
zc&*R5wD-E~fbEmgI}qE_xHGIL*jy{p)_GA7S=kE0p|N;TTcxk!@QkB=5I9vaH=8lr
zfg(2dfLp=)X*%6-%84G4Q>T}<PxpNnoz5~6QxWH=0(dQ^khAvivxi*zn5?l)3pIP8
zZs{u<g|VEzCR<f^#E#$p{~IyM+t{D7|8EcWzxMz8k3jqW?*Sjj#{X~Nwcs`20MOk3
zkAT;M+rX{hOW5|B>+gd$xDHH!k7LjO7<emq0hj?#20GX8ec1Hc*YB0!7BCI|0$ctA
z;3t9h@_P#SW9<01f>(oAf>(gO;EUMu?*{JzcLVL`|5R`_kbVCapxFL%;7Q=U*zi9N
z-T=;lXM;~+yT1i!@4f*z2d)9{$A*6ocr!Q(9C$Q%FZTO;z#Bmi+z37k4SyVnmMzh9
z<P#c72c=rbEBa->zrNEv?234Wvo-W{l)R3>Q6N?9UG#=C+(8uB)#Q=#-rL-jly+oF
z8#npj89Pfg9Ml?^#@5pirb{oLN}H(YsLF5U*a|$Bi=8GL(Z^kq<Jh7q6z^)kS$Ka6
zb4{ZV{O$JH0Vlc`Y?^R=r+a1|eU&zF$+O;Rd56+rFol%q9y&ZZ7Q|h@^LkM!Y7&JW
z5x2V|jLvTnPH8j|k@nm6H`sB|_70Ce*|aT=dRw95aeP#jC3o4g*>7XxTPo5gDH?ej
zdH-?TwgsWdWT-aaqpOeEZN1i#uU<mciZvA|pwa}&1qCU0Bd5`rgB6a4vvKV;mBEe$
zxt*GO8^>ESR`n2fE%OX(Mx;SfrUOAjMM&}#<`K$#A*{_dLl<qr#_55wnX~yr#l^wP
zY&z0d=8S7A3CYY*0+O-8zEJjf`z*dr-Jgg?a$NJ&>kPVRSdsUgbGI=BWHvIj!^vX4
z(@+Jj>V#O;mQiyhRH~b`bl`TKbJQUFQn%yxnHPC1+Zc?_SjrZ>OmkSjTj(htwFGVE
z)tFplOV2c$&o>bDlg7JY1&3N<!E485($@#D0|g&$0za^#>jaZatl+2NWW-dtVH1r0
z0APP!g|-{=kCaZT41RO<A<k`MZZf_brYWs$GF&h6r-w%MBTb1%M4fP&oH@>C`|IpE
zIKs`d9E__2sBOdF(bB|I;e6Y9S?AsFdT|-&ds~O=*)hOr#)Z~L;>4~^_^v-;fllm2
zT#o}9cC&G4P@>b5Cs_+L)tQ$?hR9UhubW<Air{41)-f>!-BbLv&iqM<htm{19V(*w
z$mu-o1qcPRjnK>NHJHhiCj@!vQ0zdHQ-wplO^#Phm+|>w2o6gJGPBUf+LD$Ls1a0Z
zUE9HuGm57~bi9G>7FxA`L+SD@n&LB&T=vu+=T~Z2DMs>*JDvtTuP5c#UW;uT)6~Ve
z+?^oBY}T&r$R|zYZ86Oes+kbv+s;Znd8pQE$~cg&<0sW!Rj!WR?itUpsp;Le53MTt
zNYC1!@f)3R;D+@c|2wBjU=M~Z&mKrT+-QL(lA6BO88mIuwzDQtxxk#xc~@JY!5E{p
zLtcxyTbI>(4OXsbK=rz_Nm2yBbknxi^V3S|FG`KxhESq4kwFqnk^TI<5({TL92H;h
zWZgO$;PD&u^QK0MO3+moVZtKUiW_yqcU|L|;)oxPW-qm#PpZ^-vuakZ6i>1oWlFJO
z(k|3|V|0l5r!S5@YCAuEd(c?)r*B*3igs01C+b|ESy0btH-nXupa@>jT;vpzDes!5
zoxp4+6zeUh#KV0p8WTDeC-knw4msOI#*dxJ&b*JEDT+P_Vx1LjEzJ_sm4W~z7-zX#
zYvIgg;PO(#o}QrD-0lgnK|ywiz^swRnzp${{wRgAprf!D+4c&LjwP8B@F(oR4uMA9
zQLmIDR0^Vhc$8r4@eomDF&rcLlfIp>HnKxMIdNE<&2~ncBi{`FKB|JnStycEhjUse
z&S^{2j2DelmPX-hdoGCxsbu2#P)JL*EW^B>?6;twRZ_;);@nuV*jBTiIKCuoN58n}
z$E9G?VWIceGRCFC2pCGu&iJSai@Gzmk!%nj2~iV;F3@B-d5X_@62&qWNtHk4tb=G6
z_S4C+qg1cds75F8WIhM2aW~l#Qk`Vr2k(}g<;@0b$Ry{G37b$aFWhDn9C1UW6R0*K
zA-!#U@Sdn>`q>bx<u8mfn>}B(e_?()@K=i0RD{jw1eXR;p(nL1t6E?-ytWC)A;KgN
z=t(rCJOCn-d9LDd-Z|IVv-jEj|32*0pO(Ff{eMTWS>J)p|5k7oXy5+{@O9wVu=^hb
z@&k0hbwG3f9|XS-z7J&J2JlDN{XYrr0juC9pmqL#jLrXg@H+5X&;oPd>EN4z`~j~A
z9dHCZ7RVQ%nEwaB3&1nMzXDf--@^y+Ch(o$9<TzI!C7zwd=5XrPk=K(zJbSpkKqUS
z2`~q~0sI|4fcJo(0P+i526upO0#|{*!55%C{@)0+=D!Y}4Yara+rgWF`~!cBAK+KP
z{a^t+0elJC{yF%4AUZz?zKoBAXZURDQ?8_^%$I~9bDYc)uG*!dds)g+(T5dO2w5*u
zP{Mu_wdR_Z;PeK_2E-1=xuiisknreQ#@4M~EMa-sR;tm0Qzmj(!JLPSa}fwSFH8%*
z^r(CJcf6nZAJi*t9U}J{XkQI88mZ7Ml$hJeMgoO`$r@DGQwP*O>)MncT7q1|;PI}J
zNHOi+!TZt9H;0VH0-1OX;YQKo9O~etzaWDIx8+Rx?%=e9M!{zpoR!?QP^@Va)K{3o
zDn2<hkrmU~N(y+s({>8pTt}4b7!Dwd^EPP+VT?4!ON}WO$ldp1Ak%G<KO?nE@`L)>
zo2s2$lf0>jI24ehc7Sd;FIs>5^KJHUp3ksXRt3P3nhJK%ij{K1{)lrrp`*C)3Fj%<
zSaAiXs%K?$tH!ta-ta)CN_;3k{_BzVQ`IXK9oib%bjEY3pXE<@hZ3|aoB<jVC^=jd
zv}ZK-=f39&m`O-)FZPg}+oPUftz{LA-6D?6QKGEWm{zy_0EUh%8g(mJI*Ef)4XEwV
z#FH<vF;w2k;d0L{)4sddOn{Ydq*wXpuFxIALnHkmOd%AGc@7#=lmzPkW$jD*2;(-p
z(C7?$*pHhA0voeH{4fc^F`a67`H6WmZvYcFQry-}+!VAqZ`DcQ_!XFNW{~m8@}XI4
zu0N`#EoW_MAqalFC`y;D6JjSuHL>;y2WAzHkTwB9YmvP4V|@z!Eo@c8LlwIf{u%zw
z<!ZqVIpbXj8=V5<b{D2nm16N-Sh~FUIFv2q%oplX$+)V-Tlo6&aDjA{yQMQ;cE_PW
zuR+|IC0Tei90UdVuM=NuiUczAudUIPmeIx(Hf4tQ)CI43iXw>zkCj6*`q4S4+(PdN
zgSY?ft4A*}Lyy{9mmM?Nic2sxOzLJ_EK2GPCR&SPB$Xl1k#_gWC)-<FpDbl!9ke{5
znx;~H`OEXQ{Vhz?8r5;si{v4kzSqY@t91#yz_kO(%{ynV7tibp4iCz9>IPvzFCGUM
zo8a8WrwrqE)l6eB`0`j8Ua?pl3yrZyV)PEdTZ-LbqS>CVr2Y~5#zt{3`*F-OdA~q}
zBw_lBSnD;=InEtQ>KfC^&01?=vDWirwV1JO^=tRj&SJhS76%}L1r^V~7f3L6j~7h_
zQ&xS{<U<i@BXN6vPMi>Yi{Yr)dpW-bUdc(9=FoAI++AiHUJb3PJgxu8z_HdGwol`9
zmC3j;$(~O|2dx$|S#ve|0|_^CJu6!Uf@5*vLGf0vgl3`OR<gWXA#GL8QQb$eQH8)2
z5i5?Pg^@a5DnuTRZ7vl8`Ro;O8$Gj&3;;-f4WLOQrR54mjl`$4;=>r9Q0j^CVlij|
zuDF&t^+LP?WjbUL?F<q2#z?n;Sdp5P2Q#&^pm{qR1&v8kzuGuDaa{jkzkMAlOY0lk
z(2H}D$@!HkV-ApbSi{((y_=liP;eZvYQSWpsi9sYM1;_mxo;`)kww52on{nBEgHu`
zc6L$sS6ofSyh7#p<)KvZ;b_rF?!?)=R4QOtHIV#PdB(bne=BBa1TVZXd!cULFAXiZ
KqTscW%KrtsZrURN

diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index 27a512a28..6b414df07 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -742,7 +742,6 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
   | EArray _ -> failwith "[Z3 encoding] EArray unsupported"
   | ELit l -> ctx, translate_lit ctx l
   | EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
-  | EApp { f = head; args = [] } -> failwith "[Z3 encoding] let in"
   | EApp { f = head; args } -> (
     match Marked.unmark head with
     | EOp { op; _ } -> translate_op ctx op args

From 8fdd39d15a8d3bd6aab36392a0e18fa57797cb9c Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 13:01:41 +0900
Subject: [PATCH 4/7] Add negative test for let_in

---
 .../test_proof/bad/let_in_condition-empty.catala_en  | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/test_proof/bad/let_in_condition-empty.catala_en

diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
new file mode 100644
index 000000000..484d00eae
--- /dev/null
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content boolean
+
+scope A:
+  definition x under condition
+    let y equals false in
+    y 
+  consequence equals true
+```

From d0ef61219f3d98026e19b5a34acc334941dc1cd8 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 13:03:44 +0900
Subject: [PATCH 5/7] Add expected outputs for tests

---
 .../test_proof/bad/let_in_condition-empty.catala_en  | 12 ++++++++++++
 tests/test_proof/good/let_in_condition.catala_en     |  5 +++++
 2 files changed, 17 insertions(+)

diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
index 484d00eae..b97255d15 100644
--- a/tests/test_proof/bad/let_in_condition-empty.catala_en
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -10,3 +10,15 @@ scope A:
     y 
   consequence equals true
 ```
+
+```catala-test-inline
+$ catala Interpret -s A
+[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
+
+┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-11:
+└─┐
+5 │   context x content boolean
+  │           ‾
+  └─ Test
+#return code 255#
+```
diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
index a5b34deba..b6913081a 100644
--- a/tests/test_proof/good/let_in_condition.catala_en
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -10,3 +10,8 @@ scope A:
     y 
   consequence equals true
 ```
+
+```catala-test-inline
+$ catala Interpret -s A
+[RESULT] Computation successful!
+```

From 5f04e0efaf12e06a3256c8f88524d53d4a84d14c Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 13:08:24 +0900
Subject: [PATCH 6/7] cleanup

---
 compiler/verification/z3backend.real.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index 6b414df07..1d8e57718 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -759,7 +759,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
       in
       ctx, Expr.mk_app ctx.ctx_z3 fd z3_args
     | EAbs { binder; _ } ->
-      let vars, body = Bindlib.unmbind binder in
+      let vars, _ = Bindlib.unmbind binder in
       if Array.length vars != 1 || List.length args != 1 then
         failwith "[Z3 encoding] EAbs not supported beyond let_in"
       else

From 8780a483129e7c90017dee0ee67f6f784700e577 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 28 Mar 2023 22:51:03 +0900
Subject: [PATCH 7/7] Correct test invocations

---
 tests/test_proof/bad/let_in_condition-empty.catala_en | 7 +++----
 tests/test_proof/good/let_in_condition.catala_en      | 4 ++--
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
index b97255d15..bf2150665 100644
--- a/tests/test_proof/bad/let_in_condition-empty.catala_en
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -12,13 +12,12 @@ scope A:
 ```
 
 ```catala-test-inline
-$ catala Interpret -s A
-[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
-
+$ catala Proof --disable_counterexamples
+[ERROR] [A.x] This variable might return an empty error:
 ┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-11:
 └─┐
 5 │   context x content boolean
   │           ‾
   └─ Test
-#return code 255#
+Counterexample generation is disabled so none was generated.
 ```
diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
index b6913081a..c3a702ec2 100644
--- a/tests/test_proof/good/let_in_condition.catala_en
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -12,6 +12,6 @@ scope A:
 ```
 
 ```catala-test-inline
-$ catala Interpret -s A
-[RESULT] Computation successful!
+$ catala Proof --disable_counterexamples
+[RESULT] No errors found during the proof mode run.
 ```