The fact that it does different stuff on Real_nequal may be an indication that they are trying to do the right (i.e., IEEE) thing. I.e., the text x != y should fail if x or y is a NAN according to IEEE (right?) and perhaps their code does.