about Z3RCF - Python interface for the Z3 Real Closed Fields package (and Theorem Prover)
Package for computing with algebraic, transcendental and infinitesimal extensions. For optimal performance, download the source code, and build Z3 using GMP (see instructions at http://z3.codeplex.com/wikipage?title=CADE24).