CUTE's paper said, combination of concrete and symbolic execution was firstly proposed here. But for single path?

1 They are looking for "out of bounds". They relax requirements to the inputs.

Sergey Vartanov, 2007–2020