diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 101de1807c..a17a1ace4a 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -340,9 +340,6 @@ is
                when Ironlake     => Audio_VID_DID = 16#0000_0000#);
       end Check_Platform;
    begin
-      pragma Warnings (GNATprove, Off, "unused variable ""Write_Delay""",
-         Reason => "Write_Delay is used for debugging only");
-
       pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
 
       pragma Debug (Debug.Set_Register_Write_Delay (Write_Delay));
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 8285dcbfad..75dde9ef26 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -61,6 +61,8 @@ is
    -- Only valid on primary pipe.
    VGA_PLANE_FRAMEBUFFER_OFFSET : constant := 16#ffff_ffff#;
 
+   pragma Warnings (GNATprove, Off, "unused variable ""Write_Delay""",
+      Reason => "Write_Delay is used for debugging only");
    procedure Initialize
      (Write_Delay : in     Word64 := 0;
       Clean_State : in     Boolean := False;
@@ -74,6 +76,7 @@ is
    function Is_Initialized return Boolean
    with
       Global => (Input => Init_State);
+   pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
 
    procedure Update_Outputs (Configs : Pipe_Configs);