  In model checking, partial-order reduction (POR) is an effective technique to
reduce the size of the state space. Stubborn sets are an established variant of
POR and have seen many applications over the past 31 years. One of the early
works on stubborn sets shows that a combination of several conditions on the
reduction is sufficient to preserve stutter trace equivalence, making stubborn
sets suitable for model checking of linear-time properties. In this paper, we
identify a flaw in the reasoning and show with a counter-example that stutter
trace equivalence is not necessarily preserved. We propose a solution together
with an updated correctness proof. Furthermore, we analyse in which formalisms
this problem may occur. The impact on practical implementations is limited,
since they all compute a correct approximation of the theory.

Logic in Computer Science