David Bühler authored 4 years ago and Loïc Correnson committed 4 years ago

The behaviors leading to forbidden floating-point values are now removed, and
the negation of their assumes are added as preconditions.