Z3.LinqBinding released

In March 2015 the licence of the Z3 Theorem Prover, invented from Microsoft Research, has moved to MIT License.
This and my current work in the space of constrained based refactoring and deep fixing has inspired me to look around for a more useful and easier API to Z3 then the default Z3 bindings for .NET.

I discovered a blog post series from 2009 about a LINQ to Z3 binding from my colleague Bart De Smet:

• EXPLORING THE Z3 THEOREM PROVER (WITH A BIT OF LINQ)
• LINQ TO Z3 – THEOREM SOLVING ON STEROIDS – PART 0
• LINQ TO Z3 – THEOREM SOLVING ON STEROIDS – PART 1

Shortly I realized that his sample code doesn't work with the current Z3 APIs.
In addition to this, some code of his samples (e.g. Sudoku) was missing.

So I decided to port his sources, combine it into a solution, add some missing parts and inluding a Sudoku theorem.
You can find it all at GitHub/Z3.LinqBinding under MIT License.