Index: /trunk/include/VBox/sup.h
===================================================================
--- /trunk/include/VBox/sup.h	(revision 54180)
+++ /trunk/include/VBox/sup.h	(revision 54181)
@@ -1649,5 +1649,5 @@
         uint64_t u64Tsc = UINT64_MAX;
         int rc = SUPGetTsc(&u64Tsc, NULL /* pidApic */);
-#ifndef DEBUG_michael
+#ifdef DEBUG_ramshankar
         AssertRC(rc);
 #endif
Index: /trunk/src/VBox/HostDrivers/Support/SUPDrv.c
===================================================================
--- /trunk/src/VBox/HostDrivers/Support/SUPDrv.c	(revision 54180)
+++ /trunk/src/VBox/HostDrivers/Support/SUPDrv.c	(revision 54181)
@@ -3917,5 +3917,10 @@
 static void supdrvGipReInitCpu(PSUPGLOBALINFOPAGE pGip, PSUPGIPCPU pGipCpu, uint64_t u64NanoTS)
 {
-    pGipCpu->u64TSC    = SUPReadTsc() - pGipCpu->u32UpdateIntervalTSC;
+    /*
+     * Here we don't really care about applying the TSC delta. The re-initialization of this
+     * value is not relevant especially while (re)starting the GIP as the first few ones will
+     * be ignored anyway, see supdrvGipDoUpdateCpu().
+     */
+    pGipCpu->u64TSC    = ASMReadTSC() - pGipCpu->u32UpdateIntervalTSC;
     pGipCpu->u64NanoTS = u64NanoTS;
 }
@@ -7586,5 +7591,5 @@
 
 /**
- * Worker routine for supdrvGipUpdate and supdrvGipUpdatePerCpu that
+ * Worker routine for supdrvGipUpdate() and supdrvGipUpdatePerCpu() that
  * updates all the per cpu data except the transaction id.
  *