An interesting technical detail is that use unsat core to generate “conflict sequences”: unsatisfiable branch sequences. This is used to reduce the number of SMT queries required.
The tool is evaluated on eight benchmarks based primarily on coverage metrics.
Papers related to Feedback-directed unit test generation for C/C++ using concolic execution
- Study of integrating random and symbolic testing for object-oriented software [dimjasevic:ifm:2018]