Checking for the bug is trivial. You can either check that the
stepping level is <8 (using the CPUID instruction) or check for a
certain result from a trivial sequence of instructions that's
equivalent to `x-(x/y)*y', where x is 4195835 and y is 3145727.
(The answer should be 0 or very close to 0 using IEEE arithmetic.)