Word equations, and logics involving strings more generally, have remained a topic of interest within the Theoretical Computer Science community, in particular due to their fundamental role within Combinatorics on Words and Formal Languages, and more recently due to interested from the Formal Methods community. The latter can be attributed to increasing popularity and influence of software tools called string-solvers, which seek to algorithmically solve constraint problems involving strings [1]}, [2]}. In this setting, a string constraint is a property or piece of information about an unknown string, and the string solvers try to determine whether strings exist which satisfy combinations of string constraints of various types. Word equations, regular language membership, and comparisons between lengths are all among the most prominent building blocks of string constraints, and when combined are sufficient to model several others. String-solvers are also useful in other areas like Database Theory, particularly e.g. for evaluating path queries in graph databases [3]} and in connection with Document Spanners [4]}, [5]}, [6]}.
