modular arithmetic bug in gnat?

[David Shochat <shochat@chelmsford.com>]

The following test is the result of distilling an issue that came up at
work:

with Ada.Text_Io;

procedure Mod_Test is

    type M_2_16 is mod 2 ** 16;

    K : M_2_16 := 11_111;

    A : constant Integer :=
       Integer(K * 1000 / 25);
begin
    Ada.Text_Io.Put ("A = " & Integer'Image(A));
end Mod_Test;

When I run this with gnat (3.12p, Linux) the answer is 51224. This is
evidently the result of delaying the reduction mod 2**16 until after the
division.

The same program on Rational Apex (3.2.0b, HP-UX 11.0) gives 1416 which
is what you get if you reduce mod 2**16 immediately after the
multiplication but before the division.

Now based on 4.5(13), the result should be as if the operations were
performed left to right, i.e. multiplication followed by division. But
each of those operations must be as defined for the modular type, and
4.5.5(10) implies that the first operation is defined as including a
reduction. So the correct result must be

((11111 * 1000) mod 2**16) / 25, i.e. 1416.

Do you agree?

-- David