I know all that. This is not my problem. This is yours. I got a postcondition violation in {REAL_64}.twin. This neither my class nor my routine. Either {REAL_64} should not allow NaN, and if it does, then EiffelBase's assertions should take that special case into account.