  The study of word equations (or the existential theory of equations over free
monoids) is a central topic in mathematics and theoretical computer science.
The problem of deciding whether a given word equation has a solution was shown
to be decidable by Makanin in the late 1970s, and since then considerable work
has been done on this topic. In recent years, this decidability question has
gained critical importance in the context of string SMT solvers for security
analysis. Further, many extensions (e.g., quantifier-free word equations with
linear arithmetic over the length function) and fragments (e.g., restrictions
on the number of variables) of this theory are important from a theoretical
point of view, as well as for program analysis applications. Motivated by these
considerations, we prove several new results and thus shed light on the
boundary between decidability and undecidability for many fragments and
extensions of the first order theory of word equations.
