xMAS is a language initially proposed by Intel for architectural modelling and verification. The main feature of xMAS is to enable a boolean encoding of liveness that can be efficiently checked using SAT-based techniques. xMAS is restricted to a small set of well-defined primitives. Recently, Verbeek et al. extended this approach to state machines. In this talk, I will recall the definitions they propose for the main boolean variables (block and idle) of the encoding. I will then show two counter-examples to these definition. Together with Alexander, we are currently working on fixing these definitions. I will discuss our current hint. This will be quite sketchy as we do not really have a satisfactory solution yet.