(I guess it makes sense to close this for now, since the VMX mitigations seem to work, and the initial bug was about them possibly not working.)