This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Σ;Ax∪E), the E;Ax-variants of a term t are understood as the set of all pairs consisting of a substitution σ and the E;Ax-canonical form of tσ. The equational theory (Ax∪E) has the finite variant property iff there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.