Index: /trunk/src/VBox/VMM/VMMAll/SELMAll.cpp
===================================================================
--- /trunk/src/VBox/VMM/VMMAll/SELMAll.cpp	(revision 12403)
+++ /trunk/src/VBox/VMM/VMMAll/SELMAll.cpp	(revision 12404)
@@ -127,5 +127,7 @@
         }
     }
-    return (RTGCPTR)(pHiddenSel->u64Base + (RTGCUINTPTR)Addr);
+    /* AMD64 manual: compatibility mode ignores the high 32 bits when calculating an effective address. */
+    Assert(pHiddenSel->u64Base <= 0xffffffff);
+    return ((pHiddenSel->u64Base + (RTGCUINTPTR)Addr) & 0xffffffff);
 }
 
@@ -208,5 +210,9 @@
         }
         else
-            pvFlat = (RTGCPTR)(pHiddenSel->u64Base + (RTGCUINTPTR)Addr);
+        {
+            /* AMD64 manual: compatibility mode ignores the high 32 bits when calculating an effective address. */
+            Assert(pHiddenSel->u64Base <= 0xffffffff);
+            pvFlat = (RTGCPTR)((pHiddenSel->u64Base + (RTGCUINTPTR)Addr) & 0xffffffff);
+        }
 
         /*
@@ -489,4 +495,11 @@
         u32Limit      = pHiddenSel->u32Limit;
         pvFlat        = (RTGCPTR)(pHiddenSel->u64Base + (RTGCUINTPTR)Addr);
+
+        if (   !CPUMIsGuestInLongMode(pVM)
+            || !pHiddenSel->Attr.n.u1Long)
+        {
+            /* AMD64 manual: compatibility mode ignores the high 32 bits when calculating an effective address. */
+            pvFlat &= 0xffffffff;
+        }
     }
     else