SPARK internal error?

[Maciej Sobczak <see.my.homepage@gmail.com>]

As a continuation of my previous post, here is the complete package with the array sorting exercise (not sure if it's correct):

Package spec:

pragma SPARK_Mode;

package My_Package is

    type Index is range 1 .. 10;
    type My_Array is array (Index range <>) of Integer;
    
    procedure Find_Min (A : in My_Array; I : out Index)
        with Pre => A'First <= A'Last,
             Post =>
             (I in A'Range and
                (for all J in A'Range =>
                    A (I) <= A (J)));

    procedure Min_To_Left (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range => A (A'First) <= A (I));
        
    procedure Sort (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range =>
                (for all J in I .. A'Last =>
                   A (I) <= A (J)));

end My_Package;


Package body:

pragma SPARK_Mode;

package body My_Package is

    procedure Find_Min (A : in My_Array; I : out Index) is
        Last_Min : Integer;
    begin
        I := A'First;
        Last_Min := A (A'First);
        
        for J in A'First + 1 .. A'Last loop

            if A (J) < Last_Min then
                I := J;
                Last_Min := A (J);
            end if;

            pragma Loop_Invariant
                (for all K in A'First .. J =>
                    I in A'First .. J and Last_Min = A (I) and Last_Min <= A (K));
        end loop;
    end Find_Min;
    
    procedure Min_To_Left (A : in out My_Array) is
        I : Index;
        Tmp : Integer;
    begin
        Find_Min (A, I);
        
        Tmp := A (A'First);
        A (A'First) := A (I);
        A (I) := Tmp;
    end Min_To_Left;
    
    procedure Sort (A : in out My_Array) is
    begin
        for I in A'Range loop
            Min_To_Left (A (I .. A'Last));
            
            pragma Loop_Invariant
                (for all J in I .. A'Last =>
                        A (I) <= A (J));
        end loop;
    end Sort;

end My_Package;

GNATprove says:

C:\maciej\temp\spark>gnatprove -Ptest -q
Internal error:
File "C:\maciej\temp\spark\gnatprove\my_package\..\my_package.mlw", line 2094, characters 208-235:
This term has type tindexB, but is expected to have type int.
 Aborting.
gprbuild: *** compilation phase failed
gnatprove: error during generation and proof of VCs, aborting.


The my_package.mlw file has explicit content and is unappropriate for Usenet publication. ;-)

Can you reproduce it? Is it a bug in the toolset?
How can I work around it?

-- 
Maciej Sobczak * http://www.inspirel.com/