Yices 2 is an efficient SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, bitvectors, scalar types, and tuples.
Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported).
Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types.
Yices 2 can also be used as a library in other software.
Download the Yices 2 source distribution. We cannot redistribute the source tarball, so you get only the RPM spec file here.