How a Symbolic Evaluator Generates Test Input for this Example
Tools that solve problems like this often use a SMT (Satisfiability Modulo Theories) solver. This a SAT solver combined with a "theory solver" that can understand operations in some domain.

For example, constraints involving = and != can be decided using union find; constraints involving &lt; on numbers can be decided using the simplex algorithm.

Operations on strings are trickier. Searching "regex string constraint" on Google Scholar finds many papers discussing approaches.

The abstract of this survey papers gives a very brief preview From An Evaluation of Automata Algorithms for String Analysis but notes there is no consensus on a single algorithm (emphasis mine):

https://doi.org/10.1007/978-3-642-18275-4_18


  There has been significant recent interest in automated reasoning techniques, in particular constraint solvers, for string variables. These techniques support a wide variety of clients, ranging from static analysis to automated testing. The majority of string constraint solvers rely on finite automata to support regular expression constraints. For these approaches, performance depends critically on fast automata operations such as intersection, complementation, and determinization. Existing work in this area has not yet provided conclusive results as to which core algorithms and data structures work best in practice.


It seems the best way to algorithmically process regexes is to operate on the NFAs/DFAs that they represent, and, judging by the number of papers on it, there are effective algorithms for making the required decisions.

HAMPI seems to be an important early paper describing how this can be done, which is provided online by one of the authors:
https://homes.cs.washington.edu/~mernst/pubs/string-solver-tr004.pdf