Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.
Download either the i686 or the x86_64 version of yices with GMP dynamically linked. The distribution cannot be redistributed freely, so we provide only a nosrc.rpm here.
Note that, lacking the sources, I have edited the shared libraries in the upstream package and generated a binary diff with the bsdiff tool, which is applied using bspatch during the build. This editing was necessary to get rid of one unneeded library dependency (libm) and to add one needed library dependency (libgmp). If SRI will refrain from linking with libm and link with libgmp, I won't have to do that in future releases. While you are at it, SRI, would you please consider adding an SONAME? Thanks!