Just an addendum: This appears to happen only when cross-compiling from a 32-bit platform, as that's the only time the (const_double ...) RTL is generated. Still a bug, though.