Z3 is the high performance theorem prover that Pex uses to solve constraint systems (and find bugs). You can now play with it too! 

http://research.microsoft.com/projects/z3/

Z3 is written in C++, but it has a .Net API to make you happy.