SPARK - strange range check with array assignment

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

Consider (extracted from a bigger problem):

-- p.ads:
pragma SPARK_Mode;

package P is

   procedure Foo (S : in out String)
      with Pre => S'Length > 3;

end P;

-- p.adb:
pragma SPARK_Mode;

package body P is

   procedure Foo (S : in out String)
   is
   begin
      S (S'First .. S'First + 2) := "abc";  -- HERE
   end Foo;

end P;


Foo is intended to overwrite the beginning of the given string.
GNATProve (2014) says:

p.adb:8:37: warning: range check might fail

Curiously, the assertion added just before the failing line:

      pragma Assert (S'First + 2 in S'Range);

passes without any warning.

What value or expression above is subject to a range check that might fail?

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