From b299a729800806b1df04b2e8edbedb449ba2253f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 22 Nov 2025 00:52:17 +0000 Subject: [PATCH] Add threading test for Z3_solver_translate and remove standalone test Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/api.cpp | 64 +++++++++++++++++++++++++++++ test_translate_race | Bin 46048 -> 0 bytes test_translate_race.cpp | 87 ---------------------------------------- 3 files changed, 64 insertions(+), 87 deletions(-) delete mode 100755 test_translate_race delete mode 100644 test_translate_race.cpp diff --git a/src/test/api.cpp b/src/test/api.cpp index 560dd1121..1cd21e7c7 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -11,6 +11,8 @@ Copyright (c) 2015 Microsoft Corporation #include "util/trace.h" #include #include "util/trace.h" +#include +#include void test_apps() { Z3_config cfg = Z3_mk_config(); @@ -104,11 +106,73 @@ static void test_mk_distinct() { VERIFY(!d); Z3_del_config(cfg); Z3_del_context(ctx); +} + +// Test for race condition in Z3_solver_translate when used in multiple threads +// Reproduces issue: https://github.com/prove-rs/z3.rs/issues/465 +static void test_solver_translate_threading() { + auto thread_fn = []() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx1 = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_solver s = Z3_mk_solver(ctx1); + Z3_solver_inc_ref(ctx1, s); + + // Create variables + Z3_sort int_sort = Z3_mk_int_sort(ctx1); + Z3_symbol x_sym = Z3_mk_string_symbol(ctx1, "x"); + Z3_symbol y_sym = Z3_mk_string_symbol(ctx1, "y"); + Z3_ast x = Z3_mk_const(ctx1, x_sym, int_sort); + Z3_ast y = Z3_mk_const(ctx1, y_sym, int_sort); + + // Add constraints: y < 2 + Z3_ast two = Z3_mk_int(ctx1, 2, int_sort); + Z3_ast y_lt_2 = Z3_mk_lt(ctx1, y, two); + Z3_solver_assert(ctx1, s, y_lt_2); + + // Add constraints: x * y = -2 + Z3_ast neg_two = Z3_mk_int(ctx1, -2, int_sort); + Z3_ast args[] = {x, y}; + Z3_ast mul = Z3_mk_mul(ctx1, 2, args); + Z3_ast eq = Z3_mk_eq(ctx1, mul, neg_two); + Z3_solver_assert(ctx1, s, eq); + + // Create new context and translate + Z3_config cfg2 = Z3_mk_config(); + Z3_context ctx2 = Z3_mk_context(cfg2); + Z3_del_config(cfg2); + + Z3_solver s2 = Z3_solver_translate(ctx1, s, ctx2); + Z3_solver_inc_ref(ctx2, s2); + + // Check satisfiability - should be SAT + Z3_lbool result = Z3_solver_check(ctx2, s2); + ENSURE(result == Z3_L_TRUE); + + // Cleanup + Z3_solver_dec_ref(ctx2, s2); + Z3_del_context(ctx2); + Z3_solver_dec_ref(ctx1, s); + Z3_del_context(ctx1); + }; + std::vector threads; + + // Create multiple threads (more than typical CPU cores to trigger potential race) + for (int i = 0; i < 20; ++i) { + threads.emplace_back(thread_fn); + } + + // Join all threads + for (auto& t : threads) { + t.join(); + } } void tst_api() { test_apps(); test_bvneg(); test_mk_distinct(); + test_solver_translate_threading(); } diff --git a/test_translate_race b/test_translate_race deleted file mode 100755 index 534f97ae821bcc1f37d0e9cad11eed0a3892bf74..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 46048 zcmeHw4|r77weLv?5EUgVv?*E{6%|EdCJ6}s4J3mTNHk3XO|5vC%uLA0WG2i^La_dc z4Omi$rB>Ab^K!j@EmdCS^|gN3R*gUnz1Ldws->3N)S{gfYN@R@wqED`*4}HMv*$1; zK)vsM-}_z;OxD?Jt-bczYwx}G+WY*w(^tDFKQGTv$2j8}L!>T{m`WyWeN1r}Mx`;& zI2C`-H9W=ypbPM;WU>?P&zA%R3z=^mAmuBjlN|7Di8d5e8WN;@ZpXYSlA@qdB-4~{ zJe_*z4-Sv`Yr)|eGOeJVPn1{B{0?~A84|Cco{wyEWR;{J`CK-f$(7hZOmwiGWG+Ir zMF|ObTQ>BtJrz{;Bysec$M$r>QYpqz(3!7|^EqKP=Tnf%pri54ROp{6ub%TAU^_bD zO{|B4s=QAjpE8xyVD!IiPNRX#b8CkpE%}M zMM*MVQYPq>&4VBHsq3y^YM@yL2*>Ih`8_hNW;0 zsR}69V;v~mg|m46jzUk*!pOu2C^#4YYcBW&F8FV|l-q!EbIHHY1;4`ue~*j&2`>CM zxaj$$i=1D%;0ImsYhCaM(7?Isdw~mnj*Ff@ci~^>!e8UUf0qmX4=!>RxY(0=Z?1Yh z?IM4X3;#@)a!nWhTU_v~pl7cB`~??%9&(Yh*QLHRh32a7$u9VRaVhsr7x|~V@W10C z|Kl!rpbZax&f{?x`JV)%$H|QJr7rkC0iVkbZ$tihIplmxw9DDXin}DSh!n)p4tTCn zY|P~OZ>B^WTOj9jL?W@d4EM+F+iIgFe?VV9N3x$JbBHSuZqh>H3ONF}yPb6khWNzX~ z#-m-~gc)oL2UoG6@M?{qi9;q$8fQ!;0$}=TY4K>%7qQL=*O;mZ$3oGX zAcT5@ZGnUdLq<}`nxN0u09<)XAQ=goahNk4Xs>B9n@UYz<6LwKC{N<*7d14-8%1eNNTOw zRZ8l>m=0OljZtw+JQ7pF=VetXkqE3cV`0_CQh{i)=J?DPY=ZITn6gjA)}R4Il@npn zZ@9Yg&J^R(GRhE3V{0NvHH4F$?O~8HHiH-jZL7@IKqP8($WCJ>!_ihyVTK_0ruIN2 z#^PGhBchR8!v@H=mLoQ!lVmCsoHdIAwYijB8AL`(c_|f?`0J{w%<_^_d&x)cQ)TYle9JI>PHNh2P5fLY`L?zMj)X4*bk2DZki(U&eTk z1AjN;n;rPA^-@k@4?_tIl~(1`^yk5k+KG-8EQjzgsCDeSQ=ZZqfMS1j?AP!xuyqV+ zcs&kEYxr3fH|(k5XKVNo4PT<+i+W^&^t?#JtNEMONz~ufQQ0HU2v2Jkb*MOi@Lq)k z+?@P!&)^(i73X?Q(eE7tI5YH~ap zp0`*8b*6@&s_~a<_>XD$c^dxX8opA)7i)OGhW~_yuh;O?G<>s$KTE@}(C}w#_%;ns zv93BgH2gUV3D~XSr)&5g4S%kN-=N|3_;<60pP}(TsNpZr@LM(fg&KaFhM%e7cWC&F zHT+Hue~E@4(C`%7t7ET*zf2*=;Ftx*EHGw)F$;`YV9Wwz78tX@m<7fx@c*O*{xbQT zzx#U+7y37j|E*~l{`CW?{LDUo@1DZlqCS~9x7=(PnG2%$J9&DgLHun*8Ga*^$+T`3 zX^LCmRwZjQJO$+Yf7CTJ~ z?coMHO$+Sdg?5@YLWaxiG%d7;&$H9Cz#cxsPSe7AINwgwf_nI!53TyrLVEZOJ53uZ z!!OxsT2K$~veUGX9{!%4rUmry!*-e$&cpZGX<9H3f8I{hLU}l0r)hya++wF`VLaSm zr)fbvywFb5LU_2$PSXN-_&hsJ3*X^0>@+QShx6_9bV|STUsnA+lzzib(}H*SB|A+E z-Qit!`g}@%&rZ{VclcpDO$*)Od#!Zlg1O5LqjmE1YD4t5%mwd#Haq>cBmI^m{kkLl zsw4e^BmJBs{j?+fgd_c3NBUci^h1vH{f_iKj`ZD*^c{|Lmm?i>q+1>7n;q$8j`a18 z^dd+48b^ArBVFQ1U+74m<4AwZkv`3lp5RD-cw=^ZzvoE5?MT1nNWbn#zv@W8kd^lS zv8M0EoBe%n_wJjL;W|&s3{9TiLwvg#g8zRC{yC2lxcEbV-x2?_Z(r+wc4VAC?>YaAAEu^2 zKsyU4%nZqXukw?B?Ya6VH$i0Qtfl_mtEYj}@b|r$n&jVj^&%wFKm8z+Nr&LAo*Vy7 z@Z~K>UaNe{KfDG+I$4T*jsCk1?}Uhue`CP~v}5G&^QFB5>GLt%{eA1}!Rp^ALEm8d zlNgl1HfLiWK#5=ySTOlz))j(jiv&!3)ergxqTB4>kuuw)Od+Iy>TTGh^7je$CrNtW z`i?C6%{Kk3lHM(glVbXH?!FhO)b9y4Uypy|7Uq#TSTn(MkL20l-?$Wfy3S2R*|-!G z9ea(yvOGa}n&vtxuJIqFwQn;r;iqRhNs0ot&K4(%&&c8*L>~O~Jg<;6f$h(-r^r@J z22{0@TEN06eK7sAzY8t4A}@Zr#9kp0=IHb7^KbNR0Nn5IUy5@nLDl1stj9J;z)zR3 zKJ2IlFzXme>v1*o!2#CmVaZz~&g= z4~~%f-0Xwt_fZ=Z<4cG9v!shjjZZ%!s4|vVZE8!n~s1d1#Sd-}b!T+qa*2$B@hf>#+qVBYZ^fh6SZXm&o+aLo>m-gT(() zVyJ)YrS!K+Ii~#&qV+G`Dbu338-ZFk(D^KN7=$Xa!;HfnPL%g^qViKWHBnNqe-)S? zk?K;h!So1f)3+aelq@nuINj9zLuF(Lf8TD!^%A)JPPXysRU{wfltah#&7v^fivGUa zNBn)AM^Kd`%Prd~?B?aWMTAa{U*Icf6HVv%`JN_g)Ja%{;tXQ4QRGP%^ans zn^Ae;AgFZF1s)bN9+Hl-9s;LUR_|d^3zU;aho$m_rMAKMY|gH2meprSW7sXLtj+oN zp!(U_Wifr7Lk`tt$%E-XQ{N*)k;=Xyvf=9jwN%qje7YRI$*lf9hjcTri~w(hnh8T8iSyVuJn9Uxc^GZqvEB^^kU^ zDx#r$Bb!No$Qeu*pjxn4Zi{ZLF9IK02jSZ;f8Rb4y7ldnxIzJB#6dS&$mC$U7`1Rn zEJcsq5Bh#8@j_`xq#Gcj4)7#@UmcX8;YWoDo2W|OjTJB{E3$q%yLlHZTd;INQzM34 zB?{OEXRsBV+x#2rNjJdCBI?BJ9!K{FVk?#YL(KLl0z^?dGS%%s(K}J}0C)z7=YGjU z_`To-4Z#8h4I7sOzWxj?!qc5_$~Ap^7CenENz#RaH&M>M=W6?YpZ-@Y&4rmsk3xSx z>(p0Yc&LHgPfg!XeCyszodSWxeig*k_Mz5;>8iidq$1TlMF`xDBs3jN-%4fmJu8#1 z`K9sShX#t_DVni+_f&p%!A%R6FSt2t^m=mn4Y+36!$p@mNZF~6I7aW#JGpvyt|3MB z6g^zXyU#`5<}7*Cg2kj9T5t%(3oCq1WGzN=h-w}cNh~{dPu?+)t&Q zN8rc_qt)N$IU4CcR|v6#mDJ*77)&9R;$8x6mVn|Tj+vqoIP`~3^cM7>-rM&XsZ!(y z3U%8^6TR>@djYAx<5vfhQ@uq{`B%)kSzeHJ&!xDU$<$c5>+n9&N1mEVGeO@EJOXSf z2GE;pKcjh8$)Rou;k=+=ErrVtSed{YJA9IjFB4qSWdPTO1jLY&~ z#KJ)8vPCS3`ue*?E?Ngs@IRP-TIQBiTHtJv99XvW`5r{40_4&C0H#KLbU#S>@1Xp0 zbnk|;7~O+HL8*qcCfIy}4bctPelY#Ga46^kDufiq?E57NZIxyb73~$`3YFbKeP0+= zmlYJU&>49x_Jev+OCf8TCQG%Qw8_SXBLA!{qS$BuJ`O7ise$NjRbnQR>a&J4dK5xv z2Db%_Xs!M!Kj8|CHp;_vz*Vm=+6+_gx2DC(>&}5|8lHkbIXvECLdR{s%(?R|<$ zGCHq=JlVjm1^KpOU~NNLfFj!62DlUHon+A(ipUOKZK*Yw{$FBMB#qxk3o2=9s%+Q6=Kl3!Qsh2hBCD{ zj64g+(Eg2Rboe6?0w3jDHQ%FRE|E`6*2pA=cn1{F!Y}gcepCWh?i@gi?bIuSofi}b z62=up1XvDml5TYOU%cDj_Zlz*G=twefUwAeRMx_3$ziIVY;*IFI2YoUW{X=Sl5oEL zX!(9}!a~<&gobC!0|HYFm;DLC&i4%^&QO@&l2Nbp4JA)gn4bf4r~oPC(ib-4(@zR5 z^hHX}scoz9L&ZV@s{dt?gauyHqAbS@r{ZOrAbW2gGE%dUJ1rVpOpr8>)Zynl@+hd>AEfb=Kb^$!7C;1C za6r0)X*yIVJ?I|AR1Ky>6B+4S_s7(!Pm^A>YcmeAYWt`;vs};FLgT^oLBRB6O7!lT zDf~{3vCUn8p7|lguL0CLkQGabpcdUuTOVk`Z07uqd=9&CzVwKl(Uz;GOWcq(8OkOA@-8HxNz&#tJ{fA1wUaG zM-u>Mp~+7Szz$e|U^<#+QKyUPVSIYln;2O4AEeeoBR@Mdjyh&5keZoM40&m-_mSb} z3B#-PLSNkg8z6n?3Y>}NxS9h&?(ZccNejUN+J7PU^7C{Xd=8x4{zCjoQ&-y$&GvQv z7-wig=d>hS+u_W`th}5$0gO7B-h?d%(GdOAZAEt-l;KhKR6HPR?JS|#GAe8R15$9~ z@*$xR#M9Mje_!!tshl;YtX|6l@|(z}c^}7ceJGoHlz}a2D$YSqo=pCzcNc7Q2CA8P z$=O1RRd_8ln7h}a=Icg1AB4|BpQKdO&? zx!PM+8}&t0Cx_H(w2*EbhwX10oxA~LedIZEe?gEfuXe1K)AhQ2^n!apMx95f&i9SZ z`X!LvJC}oMsc83ALOHsNBZ79+8W%3JcidR0@|RhDsYp2ts>x-es(OAl6;d6W6l4&0 z;qaZh9dguE)uVsvi}RFuiS0Qr>ZNI98e-!yy6J0lN2*i zEM{c(jUv;n(MTp76D9(6HxmjUJH{+9W`Qvaj9FmJ0%H~!v%r`I#w_svu?6V;6LfSN zYmFxHIv0=OSs71xI%DDPj&Lv)4tWxINk=qw1qd@OT;qbKi;bpmGUW-z+dJr;Eg>OC zzPICwDlj?*LHH*b7V|?Pkov>$(yRsRVGU%O9 z)j!W~|2iybrJm8F%Gno|Nsjp-*)wob_|1Yt91$f}KOy(f)?*JBH2{z$Z znam784`4OmHGuR2yv2a)026?Z0B!@^1Nai)LBLB7AV1{Q0?q(@5U>q!0B{4~5a2ez z3}6wicz6FglPLu>Ue9Fe0m}e80M`ND2lzVRPQa6~a6AaO46tCLVSEd42H;zO)qp4e z7Wx5B2V4hO2KWeI2yhQz3h*G{bASc7u)iO02H+n6s{wzA9lH)d54H_A11<#I0oVk% z5AY7aBY=1PK9iYpl40xxtN@&fecC3#TEGM6;7n|}zYJK4%NBTXiLngO z19&@NCE#|z6@X`Ak7ga<1%QtLRs-$N z2D}h(2jG_h_W}MJ;1R%LTzZ^>=Rj@+oCo*>U^C#$fZc%a06qv<@F&~ z;Dy*8KO4`D)B{!m#sNcs_W-T~+z$8%;M0J60Mmd60nfzMjsiSi;su-mcmrTHU<+Uf za2?<}z()Wd0el*858wg7gMfbrESQWpv*6y58GvU2Rs+rl3<1^xt^>Rk@DadA0rvpD z0C*7aZNLItBl#ruG-m)_23QTa6fgvM8{j&?uK_*+xE*j0;6A{EfNuj9;CUDI4v4&4 z8;rc}qP(*vO)T7ujXA>8<0aenWil568r2h#3*!vG3jB8b2ik{R&S^!9PAgtK`II$< zJ;t@u=3i1i<2+zRe!AIxpM|0?w&~A<{u=1h01ZX|lubVj^vj@&_dqE6Qky;r^?nI-bSpdm zLYsam=ud+_Q>U9Yy%zN6K%cAA+iiLj^aG$@qSFI5eG}+ZKiX5X^v{?Ff`RfJ2K`z1&p!AwOTNE%+_>%n!9!)xrNx;j!>x{`pqGM9j}loj zmf1SgAA?TW@@}oK6}@fZ*FSSHy1wdj)VJvOt^dqq7D3m7%g_?4oqW)9UY@1rPL%U| z*oxlAXz}ECSaf<%Z6);FkVU`KqK|;S4RqQRv+}pedU$}MzV<`VKLuFu1RRypBi}EW zh-V*uY4A{c72L1$$TlMz{uRG-_QSVPeY!NBCHIW$FW5A`cfz=0s+H*fn5WLcyp^l{ zMEirj81#C`wDq~psuRtFw}Orfbv7M#Tg~zhgZ?$p$;MXx&x-6~e9^t~4}mV;|Dx(! zYtt_U{VSl0_sl4IjZLow{ch03`+*caV$-9bKL|S9mtFoMo4yJ34WKvZ^n6)>s6XgG z9Hso{LEr8|r?#LgdsM%DutUK=3T+*(x7y;#aZrcKD#l#C5Oa8ImM+VMvP7Q;`UcR? z)#=T4U7A7vBIs_m>IVHb&~y0$4`eJHu3g5D!4pOtu}IeeJl$M} z1E6mLy-ug+S6g-X0Q4t8ck@?gBQDtodL%3V3M>Crpije2`5c`dwe`CR^vgiMTBoNZ zo!W!m)msaCA&reMA&60Zrlx<~rh?w_`S01Xwn5fR#6%bBvSf3JzPlIn63{Qw={MW? z)1c1*{W6{2D(N2J3Q>GD=qq*lb(_ZZ7UT;LOKpBBc)kE0w>GT>eJ$v2zA*}VH|Vs3 zZ`HL)>M#Q+589&(bebOv9)QBi9@OrvE9vol$k_$HTz!Y=FN6NP3*7_yUqOEr^fsJl zm2snOuVM_3X^0{3(s}Z!XUVyE9^h@DyV;@{^cd)?vhufB`MW`X(j~tKc^(A)G0;2p z{A7ofQb*$XF?c=zPm7a>ZA!Kn0?!q1WHNNMM6WAN%S6Yk@r-4lyTt?^(3?h~SAyOE zx|pYD{iG#+j4o`mUX9C+MpaVh9jjvKuebOUrZTSP&B2X(mwY)&1?7Mno-0Q6Zp zU3M86|A9Vnl=7bkef%i&!=O|B-1MV$$a^T?&8O4)WCV1#@lER%qPxYPQP8RWZuZ** z`jJuS+d+RDbhr8QdC-3ix?BAYgZ}eT*#d|7wP(GbI7Hj zkJdi5pi}#}l^+Ft2z2uGR{z)HuT7vI1l_HFYzLj}lS@8{#M6+cEc~~;zI@|}d`u-s zs^2M(Euh|u zuHJ*L%2MwiSMNJl?>ATPGgo}a3)TD16+a?Gar_td(CAQUdS|?zrgzlqX?iC;9SFhY z;gJ9#tvC);OQ_xrt=_G?L*h0|QGcZ;E?0^49ZY|p)2du9?!OJF z@0>XWmU<+nl3_i=6%0EV_AuPca4W+d3ra{2t#~qMjS;9Jq$}3Rx+$-xPoB^ z!ybm48E$2`gW&+feGG>f9$~0Hj#G4=)WgHDlwl>qdWI_)b};N=D083q-@=~kJorS$ z6`q+(TRLN@PLH=7pSUQUJ-1UN%kC(vC@HPDn90M)03ud`Vn{vHjmWjNk0Q(}NRv_>$6>9r$L(-|N6{ zVEk7c_{SN4p9Ak^=idl^c%v3oBOB(b*B`-8t){-?XL09~{-3bEU#RdW3H&t64=Vh0 z;Ln4dJy%JL*z3mW<-m)53&qHA0rUUED-nvPhwySxOM^BcNqV{ zEXk<+=2MJcAvTQ+LtI-0%aDtlzW{$am!$)Gl$OfvStzk;9;#*h*A_^;(v$8*A^z`| zNxZ7pcE(pSelizAZw(^;oh)DJe>vtQ!aMDG1Mo^Fix7am%R>C$W&5c5-T{1(ah6fs zqjMX^dgi}{^;hM-!uV^r9qF0`9p_>~%~kHzz*D*T4m*Sx|Bcx)zu4Qu={+uTzQO!& za62kH?{MMYkAT60dKo=ZzWTch{HK$qJYG;8alFX#4{*Iyd!2>A;9T&lct>0>Kn{9m zRId8o2|U&J1MYz5vizSiKE?H&$@n}>{KT)~GA0`ffX^lWX6CiJd=>ay<$g!ti;M&}2wnfD5i@jFi_RBzTgVUNY^Oon2G=~m;ToRPj+Z3k$f8@FxCTqdj46~_kkE~+{^rV z+>UBo(ASi5$$yIZ53qc8m&Uum=lZ_hS(9?hxeR#H)9HVfGXBSoaoWxJ)5@gg42&Nz z-svCmPK7?GZ&8orN4F8jCxNGOo2zA7**O4wuKISm;Cooko&{3QED4OCGX75PhvK>+ zXyXuPpOJsMq1G47Zkz->=~KprWH(`y5Wiy5;1cGaTq%)id<9(i?_>TKxL+xm`x#%) zhHT(6&csAO`Z(v2D;e*cziwu{(+~Uy<9{_<3KsXr;51c~yIwuOQ@N*ICiy?b`aH_` zNj$JFWc(|NpY>;8oPkO64Cc|nEZ|B0tL!(Ro;X&!@W0CZ&i0)S;UwqZt7Lvw*XUyW z2JR0^haHS}`p;i7-Z`#6VEoMaQhr1NqY42QmFx5~2QcrP0laa6WK{Oq#QaWsKEe2} zIs9iKLNui_7b!rk3;t%{NuNj9Ki6@luK-VeK&}7P`tcx{4JUHETgey2aVo$<5S4yvpt8Sk8z$9+teyMg=RO0MsfjQ1D^bLaZfgWgymdQDe=3RT#ki4*=LDEpNAR$L+-G29~d2P zFn-#lG7UE_j#JQZx%8jrg1^WGUj{tsvw{8X43-~bd?EV>599AqlU?~IeT0Izh=b3DZS&i?SY3;(Z} z|KC|pCG#XS9O=1}0|yLeah%S0=Q`y|;8k8-pK9RA--?X|5LEx{WjRN#mfR}uvo3O8 zVE!A~{^EW=WX(edP2kn@Q8E@)An#NP=#@qeEC2{(iB3gb(8 zTwEgAjdy`pHe{3l6Hy!XZ(oZnT1tEdI*T=hC$Q)X*YZ>0W+D&_mjpXH@a1JZIE61ghr%g*PPrT(sK!Ul z!z=MY@>CpOSq?zCNYd<#B_k_i;ZV&jKK@|z@n>m2@hoda7JON{4C*AIY$_5ryXfgH zaavOw_4@EDRRdU+|lY8Wz;~OyBj@^g(#@y6cykK0hP<)eVMO z{h8|*)YViO=5@61)-mqvoMRHA`179!C#-h9%94Lqf zR(={iHCH}m2lMiG+8YBkjriEPkH0f+YgOfCNx42GUMW73&ELSrC#yxz!q?CJ`0~5> zMtMzbd#SJ9mZrYyUfWXY^9iHKEMBvTp3#$!?@=E0upW3Cmf(Z$!ep1X#uIA-iBL@g zef-^bLz7A7%VDm@GG#ATX^ttrV=f*i3}E=#6<0NuJ#S?=WwwQ*_=-9-_tIzSogbe+ zx-P!O_2{!**ZrhU{IeA?NkRJK#yl8SPPZ)1RtlYDyv!C z&{z(czUmIN3Uq5s&4<`_D4hy-IqP-QBbim+n%WkOZ~S0OZf|PZGIN=D98`8D%N(k= ziXMbvg<6=wc&s(DQksR0OkJJ~431~6K zbqErV5yM!bQ**=8a6BG&5R7tH5S7FP9*9P64a+fLmX(y1%*pDc+`q{2>f@wDx>LKM z+aoo{YF8f~e9qM$Ff+lod*_5AtvsQaVlqJ|m~S>#seX{TyD?P} zj)kH%LDa`f0S-k)kyNrK2yX*ic}pM}37YX_3QwH3W3nZ4HO@8l_TX-*_cngkTn&U{ zIts6H5!7u<|0!pqjXpK5Rq@Iv&Jn{(IrM+B9IuyV!rYSsoVA#L7yINKOfJ7v`usA) zlG1fW!?BgAHZz<^#1r*Pf(}bIrlK(Z3ATpqRw+`VcsUt2+X86VuxR6XW;FudM0~9_ zxp&oLHj;4{=7&_cJH_pIjEN=N=kYAvw9HmPHMU+c8nUu1sDU>cn8~&6E%B(`bKJ(m zakQ!xC>(Q6!~o(sllrGgF44}+6XOZ`Y_xdx{9gU(63n6{n1s5!O$1BHI61l0TC)r5 z7z{U<&&&#?5CoF{9z9YjvmzyX99zp5vTP*Avo|eZP=}*p#-rN@e9j1t=Rk_cg{~DQ zLIS*I0+EUtFul5$m2)P=#pvNpCY&24ga$-&hFF-%mbGSB=SVDv)1gAlXrv{Ga3hdN zndFgVpTSg6ULiCnN0?O8jwu->l+k~IEyHq43j@RwkUEeYS&q44zQ|G`mlQeT?c-Qi z%u&<8v4%#u2pcUIUXOJHuPSmiiHOuW;!tz8tHtbr@ZU47m!bKO^4N}P9g_nsp|r3; zEX2^2=7&YdZAMyanv)5HQdsWCLS_x7MV!XsDHEQCgzSOlw{oUC_7;udWG& zyJeTES=^lLz&et5J9vbnNxAOF-Y+Ouq`3!E0z|&E7=9{u+g7)`U5qJ)Ubn@|K0s zSFs(A9hTrK#I`a>!CJ5s_LCb}c7v2vV5sr@77BMHv8<)7q(o;76Q7Ltv44&orbLR9 zycGqSwckXRE2oWidMTM4mR%|&M%ahSTf}&(Eu5ew6{*5IpW)S-K3M%g(T~)b*&!nK z3C259Sp!sPEwCr>0R0Ds z5`M#8!egJ@+In(rp$cjk6_l{IPyr2OJ3{{x*r~8wNI60uN6;R^&DbS?lcvFW88RBxsKg%aeCny5S6L7aTV0|Jxyo%3HEcU1_r7mN(z?q1ko(GQ= zRUA*$A&e?Lad>r>GM1miax9({u83CSi9lj4+*Tx&y^Jn*y@F+h%FeNi;H{oJ#IYhJ zu?r)$jM5rT-%dKgUL>w1(RTE)%;eJYQVV%agzPoi8WCmGA&S6uDs4T`j%^U_Mf>+~ zbvbtLbLzaqq!n+xK4HLsP_w284S7T8noaap6P%Ea?uQX={a@4?dT4e;hz)S_x3-j~&a0AClv0M#gt{ee-g7+X`_(c3!5 zKhe;HhiiO}R+iVtx#g`%LOR8)naOTT>^o##r8=Q$Tk|Bs4kD~E1ECOlax&g(htxjA z(bDpA+cVWh`%U6?ymQH`BOFv7C|ezOJ8ETH+XIepMHqBtFf?Jr_sec@?u^~tSkakwR=k`f(83HDjTCAipK(vgVcQbTI3hHB}I zL_@P9Ax7Z}@@%>pOR%>El5IvwXl)EdNSI1U3RZ8)NIaI6FhPUI3s43=>%c5sBG$kq zI4!|@uMKgM3-gxmOjthNxOsT7I{2F-AHFx-K=v4r;(Qsu2$ zhLEAoNe-z2kwWD_djw@k>4=bw65KFG3t;^wwU2O)+jnQ~v<)bdSBtpXTxv9O42=N3xyDk2`$DLC=Fw7L{MU zPe4KS{s74>WvFw4tMQ{}^HqNJJidZ$%&hcRdcOa?f-^%$F zTyc!@pLFC`&kZSf0QX(%hbmX$p23M;zIvWb!BZ6@L#O?I!uc&V>zR?^uN?V3j`Yuv zrt(#O^_;kZH}QB<*_`E*d_DiXCdsMb^NtFr{-@-<>BwKuA}I=XD@KOS^8W@r9=)^P z-=W?wa%7dv;4Dw26{P#}Cu{lD`$tBOGyi1dr}|rFx=ogAL?vwFqynm3l|CDpY3!){ z>OC86oZrI@L*t(gm0$Iv$AHtzSMM*`5EJZ1Hxac%N*ilqv{Q01THz^m%$&{2fQ;pg)AO_2g<7*bu7 s{;FPh+}P4xa>~EO>m{tg{pb3j%2l}2aiZ$3a0CO7%G7*E21nBP-^4*t-T(jq diff --git a/test_translate_race.cpp b/test_translate_race.cpp deleted file mode 100644 index b96db81b1..000000000 --- a/test_translate_race.cpp +++ /dev/null @@ -1,87 +0,0 @@ -// Test to reproduce the race condition in Z3_solver_translate -#include -#include -#include -#include "z3.h" - -void test_thread() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx1 = Z3_mk_context(cfg); - Z3_del_config(cfg); - - Z3_solver s = Z3_mk_solver(ctx1); - Z3_solver_inc_ref(ctx1, s); - - // Create variables - Z3_sort int_sort = Z3_mk_int_sort(ctx1); - Z3_symbol x_sym = Z3_mk_string_symbol(ctx1, "x"); - Z3_symbol y_sym = Z3_mk_string_symbol(ctx1, "y"); - Z3_ast x = Z3_mk_const(ctx1, x_sym, int_sort); - Z3_ast y = Z3_mk_const(ctx1, y_sym, int_sort); - Z3_inc_ref(ctx1, x); - Z3_inc_ref(ctx1, y); - - // Add constraints: y < 2 - Z3_ast two = Z3_mk_int(ctx1, 2, int_sort); - Z3_inc_ref(ctx1, two); - Z3_ast y_lt_2 = Z3_mk_lt(ctx1, y, two); - Z3_inc_ref(ctx1, y_lt_2); - Z3_solver_assert(ctx1, s, y_lt_2); - - // Add constraints: x * y = -2 - Z3_ast neg_two = Z3_mk_int(ctx1, -2, int_sort); - Z3_inc_ref(ctx1, neg_two); - Z3_ast args[] = {x, y}; - Z3_ast mul = Z3_mk_mul(ctx1, 2, args); - Z3_inc_ref(ctx1, mul); - Z3_ast eq = Z3_mk_eq(ctx1, mul, neg_two); - Z3_inc_ref(ctx1, eq); - Z3_solver_assert(ctx1, s, eq); - - // Create new context and translate - Z3_config cfg2 = Z3_mk_config(); - Z3_context ctx2 = Z3_mk_context(cfg2); - Z3_del_config(cfg2); - - Z3_solver s2 = Z3_solver_translate(ctx1, s, ctx2); - Z3_solver_inc_ref(ctx2, s2); - - // Check satisfiability - Z3_lbool result = Z3_solver_check(ctx2, s2); - - if (result != Z3_L_TRUE) { - std::cerr << "Thread " << std::this_thread::get_id() - << " got unexpected result: " << result - << " (expected SAT)" << std::endl; - } - - // Cleanup - Z3_solver_dec_ref(ctx2, s2); - Z3_del_context(ctx2); - Z3_dec_ref(ctx1, eq); - Z3_dec_ref(ctx1, mul); - Z3_dec_ref(ctx1, neg_two); - Z3_dec_ref(ctx1, y_lt_2); - Z3_dec_ref(ctx1, two); - Z3_dec_ref(ctx1, y); - Z3_dec_ref(ctx1, x); - Z3_solver_dec_ref(ctx1, s); - Z3_del_context(ctx1); -} - -int main() { - std::vector threads; - - // Create multiple threads (more than CPU cores to trigger the issue) - for (int i = 0; i < 20; ++i) { - threads.emplace_back(test_thread); - } - - // Join all threads - for (auto& t : threads) { - t.join(); - } - - std::cout << "Test completed" << std::endl; - return 0; -}