|
|
|
|
|
|
by westurner
602 days ago
|
|
|
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.) |
|
|