- to_real x = 0 does not imply is_zero x, unless x is finite.
- Add missing triggers.
- Move any property related to signed zeros from "_finite" to "_special".
- Fix incorrect signed zeros for addition, subtraction, and FMA.
- Remove inconsistent signs of NaN for negation, multiplication, and division.
- Add specification for special values of abs.
- Fix useless specification for sqrt(+oo).