I believe I have found a potentially serious issue in Vivado handling of FSM logic (I use Vivado 2018.2, so it was observed in that). The issue can occur when an FSM is specified via a unique case over an enumerated type. Depending on how the logic is written, Vivado doesn't always treat such RTL as an FSM (as evidenced by a lack of inferred FSM for state register message in the synthesis log). In that case, it appears to treat the unique specifier as a hint to handle the logic as a parallel case (as evidenced by implementing as parallel_case message in the synthesis log) and the state register sometimes gets implemented as 32 bits (as observed in the schematic). Somehow the combination of these 2 things causes synthesizer to sometimes optimize the logic in a manner that breaks functionality.