--  { dg-do compile }

procedure SPARK3 (X : in out Integer) with SPARK_Mode is

   procedure Q (X : in out Integer) with SPARK_Mode => Off is
   begin
      X := X + 1;
   end Q;

   procedure R (X : in out Integer);

   procedure R (X : in out Integer) with SPARK_Mode => Off is
   begin
      Q (X);
   end R;

begin
   R (X);
   X := X + 1;
end SPARK3;