diff --git a/xen/arch/x86/hvm/vmx/vvmx.c b/xen/arch/x86/hvm/vmx/vvmx.c
index 5ef5ad7385..f385c02282 100644
--- a/xen/arch/x86/hvm/vmx/vvmx.c
+++ b/xen/arch/x86/hvm/vmx/vvmx.c
@@ -1826,7 +1826,7 @@ int nvmx_msr_read_intercept(unsigned int msr, u64 *msr_content)
     switch (msr) {
     case MSR_IA32_VMX_BASIC:
         data = (host_data & (~0ul << 32)) |
-               ((v->arch.hvm_vmx.vmcs)->vmcs_revision_id);
+               (v->arch.hvm_vmx.vmcs->vmcs_revision_id & 0x7fffffff);
         break;
     case MSR_IA32_VMX_PINBASED_CTLS:
     case MSR_IA32_VMX_TRUE_PINBASED_CTLS: