@lizzy My theory is that their optimizer either doesn't save the precondition rax = 0 for the branch, or it doesn't correctly map eax to the lower 32bits of rax.
From my quick testing, it seems like theory B is more likely, but then again, I don't know _that_ much about their internals.