You might also want to look at the Decision Procedure
Toolkit (DPT): http://dpt.sourceforge.net/
DPT is an open source (Apache 2 licensed, source forge
hosted) SMT solver implemented in OCaml with good performance. The current
release supports only SAT + EUF, but future releases will soon add integer and
rational linear arithmetic – of course, you can always add the theory you
want yourself.
Kind regards
Jim Grundy