[cfbolztereick]

I only support integer operations in the DSL so far.

(but yes, turning the python expression x*y+z into an fma call would not be a legal optimization for the jit anyway. And Z3 would rightfully complain. The results must be bitwise identical before and after optimization)

[westurner]

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.)