blocks: 3  (solved 1, certified 1, candidate 1)
residual constraints: 2
  [solved] definition  (1 constraint)  cert=definition_decoder
      decoder: q := r && s
  [candidate] guarded-next-assignment  (1 constraint)
  [certified] mutex  (1 constraint)  cert=mutex_safety
