1--  { dg-do compile }
2
3procedure SPARK3 (X : in out Integer) with SPARK_Mode is
4
5   procedure Q (X : in out Integer) with SPARK_Mode => Off is
6   begin
7      X := X + 1;
8   end Q;
9
10   procedure R (X : in out Integer);
11
12   procedure R (X : in out Integer) with SPARK_Mode => Off is
13   begin
14      Q (X);
15   end R;
16
17begin
18   R (X);
19   X := X + 1;
20end SPARK3;
21