How a Symbolic Evaluator Generates Test Input for this Example

Question

Say we have some complicated function that determines if a string matches an XSS attack string, and throws an error or does something else in that case.

function somethingWithXSSVulnerability(x) {
  var regex = /<script(.*)>(.*)<\/script>/
  if (x.match(regex)) {
    throw new Error('XSS')
  } else {
    return x
  }
}

In trying to understand symbolic evaluation in regards to test generation, I am wondering how it would generate a test for this case. How it would generate an x such that it matched the regex. It could be a lot more complicated than a regex, a grammar for example. The test case generating the error would be something like:

// yes case
somethingWithXSSVulnerability('<script>alert("foo")</script>')
// no case
somethingWithXSSVulnerability('anything else even <script> w/o closing tags')

To really test it, it might need to generate an alert or try setting a cookie or something, so there it is becoming even more complicated.

But I am trying to get a sense of how the symbolic evaluator generates a test for this case. How it determines the value of the input to the function. It seems like it would have to understand the structure of the regex, then reverse-engineer an input to match it. Wondering if that is so.