It seems to me like they are only open sourcing the products they wish more people are using, and not their actually useful products like MSOffice and the Windows OS.

Edit: to be clear, I know it is in their best interest not to open source those products, because that's where most of their money comes from. But it really looks to me like the want to flood the market with random open source stuff, so that they seem more open source friendly. But in reality they are not actually contributing anything very useful to the community.

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.