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.
Page rendered at Sunday, June 03, 2012 12:18:11 AM (Pacific Daylight Time, UTC-07:00)
Disclaimer The opinions expressed herein are my own personal opinions and do not represent my employer's view in anyway.