Exception transition rejected on message assignment

[jklmnn]

The state Start in the following spec assigns the return value of a function call to a message variable. This message can be invalid yet the model checker complains that there is an unneeded exception transition:

package Test is

   type Data is range 0 .. 255 with Size => 8;

   type Message is
      message
         D : Data
            then null
               if D = 42;
      end message;

   generic
      with function Get_Message return Message;
   session Session with
      Initial => Start,
      Final => Terminated
   is
   begin
      state Start
      is
         Msg : Message;
      begin
         Msg := Get_Message;
      transition
         goto Process
            if Msg.D = 0
         goto Terminated
      exception
         goto Error
      end Start;

      state Process
      is
      begin
      transition
         goto Terminated
      end Process;

      state Error
      is
      begin
      transition
         goto Terminated
      end Error;

      state Terminated is null state;
   end Session;

end Test;

Parsing test.rflx
Processing Test
test.rflx:29:10: model: error: unnecessary exception transition in state "Start"