Index: /trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp
===================================================================
--- /trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp	(revision 88320)
+++ /trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp	(revision 88321)
@@ -542,5 +542,5 @@
  * @param   uReg    The 32-bit value to write.
  */
-static void iommuIntelRegWrite32(PIOMMU pThis, uint16_t offReg, uint64_t uReg)
+static void iommuIntelRegWrite32(PIOMMU pThis, uint16_t offReg, uint32_t uReg)
 {
     /* Read current value from the 32-bit register. */