Solving equations involving terms with variables that can be instantiated to sequences of terms (sequence variables) and terms with function symbols of arbitrary arity may lead to infinite loops. This is particularly relevant when the implementations traverse the solution tree using a depth-first strategy, because some solutions become unreachable when they appear after a branch that loops. In this paper we present a simple method for checking if a branch will lead to a loop. This makes it possible to go on with the unification algorithm without trying to explore those branches. The technique we use is based on an abstraction of the original unification by a Diophantine equation on the sizes of the terms involved. We present this abstraction and show that it is correct with respect to the original unification.