/* |x| in [log(maxdouble), log(2*maxdouble)) */
if (ex == 0x400c && (mx < 0xb174ddc0u ||
(mx == 0xb174ddc0u && lx < 0x31aec0ebu)))
{
/* |x| in [log(maxdouble), log(2*maxdouble)) */
if (ex == 0x400c && (mx < 0xb174ddc0u ||
(mx == 0xb174ddc0u && lx < 0x31aec0ebu)))
{