Does Z3 distinguish between x*y+z and z+y*x, in terms of floating point output?

math.fma() would be a different function call with the same or similar output.

(deal-solver is a tool for verifying formal implementations in Python with Z3.)