Workaround for invariant SPARK condition

[xorque <xorquewasp@googlemail.com>]

Hello.

I have a piece of code that does this:

function Check_Support (Request : in Request_t) return Boolean is
begin
  return Request /= Unsupported;
end Check_Support;

I'm using it in some code:

if Check_Support (Request_Push) then
  ...
end if;

Request_Push is a compile-time constant with an implementation-defined
value. Given that the value is detected at compile-time, SPARK thinks
the
condition is invariant.

Is there some way I can tell SPARK that this condition isn't actually
invariant,
even though it appears to be?