Just skimmed through the paper: https://arxiv.org/pdf/2007.14049.pdf https://arxiv.org/pdf/2007.14049.pdf, it seems like they are using some sort of heuristical

Just skimmed through the paper: https://arxiv.org/pdf/2007.14049.pdf https://arxiv.org/pdf/2007.14049.pdf, it seems like they are using some sort of heuristically mutating a test suite until it's fully branch covered, based on calculating `branch distance` for each predicate. Why isn't a SMT solver like Z3-solver being used here to solve for the predicate (generating inputs to evaluate to true/false)? Since it's getting so powerful, and python container/dict/string(regex) operation can also be modeled conveniently. And I'm also wondering, whether there is a return based automatic test generation, that start from the return value, and resolve all variables used and gather all possible return values with its constraint, and feed those to z3 to generate inputs to cover. It seems like it will help with branch explosion by eliminating unused branch, and only focus on branch that is being used. Edit: it looks like CrossHair[0] is a similar tool that uses Z3 to find counter examples for predicates. [0] https://github.com/pschanely/CrossHair https://github.com/pschanely/CrossHair