X86_CR4_SMXE
cr4_fixed1_update(X86_CR4_SMXE, ecx, feature_bit(SMX));
TEST_INVALID_CR_BIT(vcpu, cr4, sregs, X86_CR4_SMXE);
cr4 |= X86_CR4_SMXE;