The following should not be type correct.

embedded_cond_bug: THEORY
BEGIN
 x,y,z: real
 b: nat
 
 f:bool =
   COND
     x < 0 -> b = 0,     
     x >= 0 ->
       COND
      x = 0 -> b =1,
      x > 0 ->
        COND
          y <= 0 -> b = 2,
          y >= 0 -> b = 3
        ENDCOND
    ENDCOND
   ENDCOND
END embedded_cond_bug

In PVS 6.0 there was a bug in a COND embedded in another COND.