Is the Z3 theorem prover an example of a CP tool? For those interested, Z3 is one of the world's fastest theorem provers and has been open sourced by Microsoft. Theorem provers have many interesting applications, but one of my favorites is using them to represent a program's state and reasoning about the exploitability of bugs. It has bindings to C, C++, .NET and Python. Check it out if it interests you:
http://z3.codeplex.com/ or try it online at http://rise4fun.com/z3py
Before you download Z3 and dive in, be aware that Z3 is not Open Source. It's licensed under a non-commercial license[0], which is not compatible with the Open Source definition[1]. Muddying the term Open Source will diminish its descriptive usefulness.
Z3 is based on SMT (satisfiability-modulo-theories), not constraint programming. You can probably do some constraint programming in it, but that's not what it's designed for.
