[tonmoy]

Love Z3. It is easy to use and very decent performance! I don't think MS is using Z3 on this product though, looks more like the smart enumeration based program synthesis

[c-cube]

I think most of the enumeration-based synthesis tools rely on a SMT solver (Z3 or CVC4, say) to learn from bad solutions.