diff -r 9dbbf1631193 xen/arch/x86/hvm/vmx/vvmx.c
--- a/xen/arch/x86/hvm/vmx/vvmx.c	Mon Jul 25 14:21:13 2011 +0100
+++ b/xen/arch/x86/hvm/vmx/vvmx.c	Tue Jul 26 12:42:00 2011 +0100
@@ -1070,11 +1070,17 @@ int nvmx_handle_vmresume(struct cpu_user
     int launched;
     struct vcpu *v = current;
 
+    if ( vcpu_nestedhvm(v).nv_vvmcxaddr == VMCX_EADDR )
+    {
+        vmreturn (regs, VMFAIL_INVALID);
+        return X86EMUL_OKAY;        
+    }
+
     launched = __get_vvmcs(vcpu_nestedhvm(v).nv_vvmcx,
                            NVMX_LAUNCH_STATE);
     if ( !launched ) {
        vmreturn (regs, VMFAIL_VALID);
-       return X86EMUL_EXCEPTION;
+       return X86EMUL_OKAY;
     }
     return nvmx_vmresume(v,regs);
 }
@@ -1085,11 +1091,17 @@ int nvmx_handle_vmlaunch(struct cpu_user
     int rc;
     struct vcpu *v = current;
 
+    if ( vcpu_nestedhvm(v).nv_vvmcxaddr == VMCX_EADDR )
+    {
+        vmreturn (regs, VMFAIL_INVALID);
+        return X86EMUL_OKAY;        
+    }
+
     launched = __get_vvmcs(vcpu_nestedhvm(v).nv_vvmcx,
                            NVMX_LAUNCH_STATE);
     if ( launched ) {
        vmreturn (regs, VMFAIL_VALID);
-       rc = X86EMUL_EXCEPTION;
+       return X86EMUL_OKAY;
     }
     else {
         rc = nvmx_vmresume(v,regs);
@@ -1162,6 +1174,7 @@ int nvmx_handle_vmclear(struct cpu_user_
     struct vmx_inst_decoded decode;
     struct nestedvcpu *nvcpu = &vcpu_nestedhvm(v);
     unsigned long gpa = 0;
+    void *vvmcs;
     int rc;
 
     rc = decode_vmx_inst(regs, &decode, &gpa, 0);
@@ -1176,9 +1189,15 @@ int nvmx_handle_vmclear(struct cpu_user_
 
     if ( gpa != nvcpu->nv_vvmcxaddr && nvcpu->nv_vvmcxaddr != VMCX_EADDR )
     {
-        gdprintk(XENLOG_WARNING, 
-                 "vmclear gpa %lx not the same as current vmcs %"PRIpaddr"\n",
+        gdprintk(XENLOG_WARNING, "vmclear gpa %lx != %"PRIpaddr"\n",
                  gpa, nvcpu->nv_vvmcxaddr);
+
+        /* Even if this VMCS isn't the current one, we must clear it. */
+        vvmcs = hvm_map_guest_frame_rw(gpa >> PAGE_SHIFT);
+        if ( vvmcs ) 
+            __set_vvmcs(vvmcs, NVMX_LAUNCH_STATE, 0);
+        hvm_unmap_guest_frame(vvmcs);
+
         vmreturn(regs, VMSUCCEED);
         goto out;
     }