Contradiction check too strict

[treiher]

The check for contradicting conditions seems to be too strict. I see no reason why the model shown below should not be accepted.

package Test is

   type F0 is (A, B, C, D) with Size => 8;
   type Value is mod 2**16;

   type Message is
      message
         F0    : F0
            then F1
               if F0 = A,
            then F2
               if F0 = B;
         F1 : Value
            then F3;
         F2 : Value;
         F3 : Value
            then F4
               if F0 = A,
            then F5
               if F0 = B;
         F4 : Value
            then null;
         F5 : Value;
       end message;

end Test;

rflx: model error: contradicting condition 0 from field "F3" to "F4" on path [F0 -> F2 -> F3] in "Test.Message" (B = 1
   ∧ A = 0
   ∧ F0 = B
   ∧ F0 = A)