The Clang Static Analyzer is a great codebase to learn from. A long time ago, before Z3 was open source, I added a constraint manager that used STP for the same

The Clang Static Analyzer is a great codebase to learn from. A long time ago, before Z3 was open source, I added a constraint manager that used STP for the same objective: https://reviews.llvm.org/D15609 https://reviews.llvm.org/D15609 It may be dated by now but there is also a tutorial on writing checkers (https://clang-analyzer.llvm.org/checker_dev_manual.html https://clang-analyzer.llvm.org/checker_dev_manual.html), or follow one of the many examples in the codebase. My first checker is still there — it just turned 10 years old, and is under 100 lines without comments. https://github.com/llvm/llvm-project/blob/main/clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp https://github.com/llvm/llvm-project/blob/main/clang/lib/Sta...