(NMI profiling results indicate this both is relatively expensive and happens a lot unnecessarily if the fpu is in use.)