raSAT: SMT solver for Polynomial Constraints on Real numbers
raSAT berief description
raSAT is an SMT to solve problems in QF_NRA category,
i.e., bounded quantification on conjunction of polynomial inequalities.
It combines miniSAT 2.2 and background theories, which are various interval arithmetics.
Main features are,

raSAT applies raSAT loop, which applies over/under approximation theories.
An overapproximation theory detects UNSAT, and an underapproximation theory detects SAT.
If neither holds, raSAT loop refines bounded quantification by interval decompositions.

raSAT is based on an interval constraint solving, similar to
HySAT.
raSAT prepares various interval arithmetics as overapproximation theories, which are mostly
Affine intervals. It also prepares testing (with several strategies) as underapproximation theories.

raSAT installation is confirmed on Win7, Win8 / cygwin 64bit (not 32bit), and linux.

raSAT accepts inequality problems in SMTLIB format (.smt2)
(including the use of ">=" and "<=" in formulae, but not $=$),
which is confirmed on
metatarski,
hong,
zankl
benchmarks.
raSAT download
raSAT usage
 Example snapshot
 "sbox" is the bound for the minimum range of the decomposition,
and "tout" is the timeout in seconds, and they are optional.
(Default values are 0.1 for sbox and 60 seconds for tout, respectively).
raSAT history
 Version 0.1, release at 22 Jan 2014
Notes
 Similar to dReal,
raSAT requires to specify an input range (i.e., the range is specified bound="lb ub",
which are the lower and upper bounds), to avoid openended ranges like (0,\infty).
For example, if 0 < x < 2 and 2 < y < 4, bound = "0 4" will not restrict anything.
Note that current implementation assigns the same input range to each variable.

Older version of cygwin 32bit also worked (with flexdll package), but
the latest cygwin 32bit fails to link (at least in our environment).
Win7, Win8 / cygwin 64bit also sometimes fails to compile.
This is often recovered by reinstallation of cygwin.
Reference
To Van Khanh, Mizuhito Ogawa,
raSAT: SMT for polynomial inequality,
JAIST Research Report ISRR2013003.
Contact
Questions and comments to To Van Khanh (UET/VNUHN, tovankhanh [at] gmail.com) and/or
Mizuhito Ogawa (JAIST, mizuhito [at] jaist.ac.jp). (Please replace [at] with @.)