Does anybody know if Z3 supports SSMT (i.e. randomized quantifiers) or if there is any plans to add it?
There are no current plans to directly handle randomized quantifiers. The authors of that paper may have more information. The paper points to a system: https://projects.avacs.org/projects/sisat/wiki/SiSAT_Manual However, it has been inactive the past 3 years, so I am not sure if this is something the authors are urgently pursuing. Maybe there are follow on systems. The closest I am considering is alternating min/max objectives. That is, you should be able to compute some objective function f(x,y), such that x, y satisfy constraints Phi(x,y) and subject to min x max y f(x,y). The latter means to find x, such that f(x,y) is minimized, over all y.