ensure that the conversion from internal timer to double is done in a consistent way. Otherwise we get double-rounding effects (show up on x86 at -O2 typically), which makes the timer non-monotone.
ensure that the conversion from internal timer to double is done in a consistent way. Otherwise we get double-rounding effects (show up on x86 at -O2 typically), which makes the timer non-monotone.