Comment by ulber

Other people are already flooding you with counterexamples, but I'll add to the pileup:

Z3 (https://github.com/Z3Prover/z3) is the Satisfiability Modulo Theories (SMT) solver to use. It is such a quality piece of software and it's amazingly easy to find help on StackOverflow from the main developers. Z3 really is the default choice for an SMT solver these days (i.e. you only reach for other solvers when you really have to).

Roslyn (https://github.com/dotnet/roslyn) is the C# (and VB) compiler as a library. Useful for doing code analysis and code generation for a modern imperative language. Roslyn is a whole lot easier to get started with than integrating Clang/LLVM into a project, so it really lowers the barrier of entry for lightweight program analysis projects.