The goal of this project is to provide a new option in the clang static analyzer to validate (or refute) reported bugs, by using an SMT solver. The implementation consists of an extra step, after the bug is found by the built-in solver (RangedConstraintManager) but before reporting it to the user; the path and the constraints that trigger the bug will be encoded in SMT and checked for satisfiability using the SMT solver Z3. The expected result of the project is to reduce the number of false bugs reported by the analyzer and evaluate the overhead introduced by Z3 during validation.


Mikhail Y R Gadelha


  • George Karpenkov
  • Artem Dergachev