From 082caae4981e793a8986b76d0ab31cdb3f8294a2 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 28 Mar 2023 12:48:44 +0900 Subject: [PATCH] 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}0zPJAsueY*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$`skFhj%Ip_*U>K zjQzKR1@JB4FEP%46xIHuE*H^Pemt9=#x^uPeRG-WJb$^{d>-~#)f|Hhhqu}R;S3sU2sc_x<6HV<~}R* zP(|`OK_thg%B%a`Q4&5(!c)p&URn4mk0(^3ZY+0VF-CAwksa;gf#dT;-Y)iAb?iL5)0(-UJt+jhiU({}P z&!Ay<1~gm8t=4+J`65@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-MDSoIajjGhGJ$HlUEolAF=x$2mwX%jMy=Vn6dIFKaE(gPZaeh0Csi|R zFC!m(Bh1oir$HK1P@e|lao zCa~WfL2OQ$>{JE^e2%+a=DDxu+gWTqpc06-<{=b_$=1oag(ulMFXG;nV8E2dka7iVsgZ6=H{f%{Tv=SlAaf2nfV(Uf$Ct zG)|D_l%#s3DC{`@6u%{Y+m$f-V=MyObqNC!$>Xo*5ANXXE@TWA7Nz(gKBa;xo- zN}t4MsR53V!n>N&Z+I1VlByTeE+ zeHSE6M!t~1fr`3dOb+Gn-bw`q8^E%sVBiM2@4@)jJi)=O=2W;IA4~i|y5fq{UgxxA z&%@RS1IJ9ETiXN2Yv(gp^{-7ILql9GX50^Qvm)2B{NpExsfoi=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+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^1H1yWtm(4h(mAcCqq4RP_cq>kN^tjlW z7}v@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@RV49F| zjD7{LVY4lEFtW{cFlFPJYpvTDN6Q2WMR9!pMku8YN_Srs=eX+eTK7C^2~HILK(C*S zf?=K-hebsUS}8S$UV27A=7cZqzsf6dL=3hKI$=*#wppCUqCMIPT5Zqhk|i* z7sFn5XQtch8ts;9ji&jkCuVsmdUNLdeH(X-{|BqMA5fepjE1oC4mXWHyVA<~jr!D# z_nO%-qY)?)}Sk8CYx5)ztJ-OVz!jcPcg%Ty~Te zX?NCw_?MB3wHQlosaL%`Y1Aj9$dsrKSxtrd%j@Rm29ZA`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)cMyqemr6pXzbB z6Q_*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{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(0Z;k*%|yNM&Nv&F}t|Zz|~2vHowhGk4rq#A3UNUl3Y^?epKWHZ+ffT%yHRag&-H%+SoHaKkh`ORK?z^ z6~0MTa3FNnf}gJFry%)_E%Hs$!@qBhx)t)Er&f(HON(Al+-Ur(_TVsyjY*eXKk4m) zf@V76<>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^JUDeN-a%W$!tC*Ji=#c6 z)N}ukrR{vUT~9Vi=(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~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=?o)zbSZ>zcO4ep2nWhYQ z*br;!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)qKFnw-|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$2FPH4h-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|E4Y z)ChKI$;QF``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 zS#^D92!ec%VcGPnyo3uu3Vr+`18 zJ>(NmyJ(*Q|50N)N1%N^XwbSxj!DDvTH~Y~*tum?Ju@xlQ~1NqoyvpsWmB_%Oiku0pbTd_0HRt3L2+j?0+=Vj<$wgJ*4GB#Vb z$7SAoSnPjAgT-4fDCaVjTzk^p=z=pW_R2!~=){^>+eoLTn7)5x_(1FjzfFzJXZUB^ zgthuGekN`#XpIr;Mz`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&aYIrq4FmeIMMrrf-qLp@JL;@BweG~oTnn139g!|tu`T{z0zP{!7C?SO7{w>?kT5g zY+^-RHK|9niU3kT9iI@MDxXi_Cn`k)PLy6 z)w6B+BoYT_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>?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&7d3h?jTiA^$Sb!ErYqKxor&;FhUT}*Q-?6Ei4c@VPW8Pr`XoEL2 zHRPvra3+}L9QNqL60R~c$cqP`;|N8h(vxo2OW1V>Y8P&(m@JADy)U~XGfQW9@Q8xS z*j$`dXXLAg4>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-RF6 z4_*ge1fBt&0=~dJ{~v*001dDJZUbM`{66?Y@Sng%puGa03a$d0_t%`i*8cAWpJZaS^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+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<=$Golm2fZAZm2s+-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%f=^@HKMZ~cJOu6seb56_U?;c+ychfaSHU`{ zgB!vB!nXfi@IyfH{x^WDfb9Ht0@?ZVK(_wVz@x#}0G$W;%i!f;1uTQ>!I!Y{KMpmOaLW`dP-vKgkE0_ic!Ob9^E$~R~ z^X=!iDX>j}Z3_IOrvO`t>DZ>34vzSl4%=#+&u*#J&$Exr%tE|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&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;IjGfjhaAuK8OXP_*n11`A6PeOBxz}H)muVwI*%)+vVvIy)XcEA-< zFl?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%>gsNi1Yf{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?a0y+oaP2eR!_WgC>Dd5x0^M3%m1uOsuo(MhztwgVv zg6{<{1AD+@!6%^Q&w)0$0sI;B`tJm<04IRX0k{r48T>JG{On72i+cRE@(?P!woBg-B18r$X`X(8|*#bS=2$ukxCr9CkjO}1#OGLL&dr` zT()gK;{0e(5Qawns7SJu3`{PbdIrB^(P z&x|#-NIxgPQnekVbk%37RP%ZicPzDYb1QmfBr7cXie1+~C^|ST(6*Vel>WPt)e7ec zp&V;@^SnQW7cE$0b=Kwh6FuAMiW7sPOriYJ&Hc7zwxtuVVT^?w)oxa6TcS6#(^K*# z@PtaZyS{-=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#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&~{V`X#cI04Gz1Jl_agvW;jo9%cernWyI zWXe6YP#k{DQL@1*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#RT}+gd$xDHH!k7LjO7(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 zzrNEv?234Wvo-W{l)R3>Q6N?9UG#=C+(8uB)#Q=#-rL-jly+oF z8#npj89Pfg9Ml?^#@5pirb{oLN}H(YsLF5U*a|$Bi=8GL(Z^kq7XxTPo5gDH?ej zdH-?TwgsWdWT-aaqpOeEZN1i#uUESR`n2fE%OX(Mx;SfrUOAjMM&}#<`K$#A*{_dLlkPVRSdsUgbGI=BWHvIj!^vX4 z(@+Jj>V#O;mQiyhRH~b`bl`TKbJQUFQn%yxnHPC1+Zc?_SjrZ>OmkSjTj(htwFGVE z)tFplOV2c$&o>bDlg7JY1&3NjaZatl+2NWW-dtVH1r0 z0APP!g|-{=kCaZT41ROC`|IpE zIKs`d9E__2sBOdF(bB|I;e6Y9S?AsFdT|-&ds~O=*)hOr#)Z~L;>4~^_^v-;fllm2 zT#o}9cC&G4P@>b5Cs_+L)tQ$?hR9UhubW!-BbLv&iqMNHJHhiCj@!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}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)MncT7q1|;PI}J zNHOi+!TZt9H;0VH0-1OX;YQKo9O~etzaWDIx8+Rx?%=e9M!{zpoR!?QP^@Va)K{3o zDn28pTt}4b7!Dwd^EPP+VT?4!ON}WO$ldp1Ak%G zo2s2$lf0>jI24ehc7Sd;FIs>5^KJHUp3ksXRt3P3nhJK%ij{K1{)lrrp`*C)3Fj%< zSaAiXs%K?$tH!ta-ta)CN_;3k{_BzVQ`IXK9oib%bjEY3pXE<@hZ3|aoB;y2WAzHkTwB9YmvP4V|@z!Eo@c8LlwIf{u%zw zzkCj6*`q4S4+(PdN zgSY?ft4A*}Lyy{9mmM?Nic2sxOzLJ_EK2GPCR&SPB$Xl1k#_gWC)-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{Yi{Yr)dpW-bUdc(9=FoAI++AiHUJb3PJgxu8z_HdGwol`9 zmC3j;$(~O|2dx$|S#ve|0|_^CJu6!Uf@5*vLGf0vgl3`ORr9Q0j^CVlij| zuDF&t^+LP?WjbUL?F 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 \