An equational theory decomposed into a set $B$ of equational axioms
and a set $\Delta$ of rewrite rules has the \emph{finite variant} (FV)
\emph{property} in the sense of Comon-Lundh and Delaune iff for each
term $t$ there is a finite set $\{t_{1},\ldots,t_{n}\}$ of
$\rightarrow_{\Delta,B}$-normalized instances of $t$ so that any
instance of $t$ normalizes to an instance of some $t_{i}$ modulo $B$.
This is a very useful property for cryptographic protocol analysis,
and for solving both unification and disunification problems. Yet, at
present the property has to be established by hand, giving a separate
mathematical proof for each given theory: no checking algorithms seem
to be known. In this paper we give both a necessary and a sufficient
condition for FV from which we derive, both an algorithm ensuring the
sufficient condition, and thus FV, and another disproving the
necessary condition, and thus disproving FV. These algorithms can
check automatically a number of examples and counterexamples of FV
known in the literature.