Unprovable code for message with field condition

[kanigsson]

RFLX generates unprovable code for the procedure To_Context (at least) for the following message:

package Cond is
   type A is mod 2 ** 32;
   type B is mod 2 ** 8;

   type Cond_Msg is
      message
         F1 : A
            then F2
               if F1 = 0;
         F2 : B;
      end message;
end Cond;

The issue is that F1 must be 0 to be able to set it, but the To_Context function has no precondition that would enforce this.