SPARK - division by zero problem

Ada Programming

While playing with SPARK (I also agree that comp.lang.ada is adequate for SPARK content) I have found a problem that can be shown in the following stripped-down example:

package My_Package is

    procedure Divide (X : in Integer; Y : in Integer; Z : out Integer);
    --# derives Z from X, Y;
    --# pre Y /= 0;
    --# post Z = X / Y;

end My_Package;

package body My_Package is

    procedure Divide (X : in Integer; Y : in Integer; Z : out Integer) is
        Z := X / Y;  -- this is line 5
    end Divide;

end My_Package;

In this example I would expect the VC associated with rtc on line 5 above to be discharged based on the hypothesis from Divide's precondition: that is, Y is known to be non-zero, so division by zero in line 5 cannot happen.

Tools are invoked in the following order:

$ sparkmake
$ spark -index_file=spark.idx -vcg -config_file=config.cfg -output_dir=spark my_package.adb
$ sparksimp
$ pogs

The summary says that the VC in question in undischarged.
Is there anything missing?

The tools come from Ubuntu packages and announce themselves as GPL 2011.                                            
Phil says...

The undischarged VC I get is:
H1:    y <> 0 .
H2:    x >= - 2147483648 .
H3:    x <= 2147483647 .
H4:    y >= - 2147483648 .
H5:    y <= 2147483647 .
H6:    integer__size >= 0 .
C1:    x div y <= 2147483647 .

which is false for x = -2147483648, y = -1


Right, I fell into the trap by focusing on Y /= 0 condition. Indeed, the assymetry of Integer'Range is causing troubles in this case.
Thank you for response.