Another option is STP.  It's written in C++ I think, with OCaml binders.

http://people.csail.mit.edu/vganesh/STP_files/stp.html

-Mike

On Mar 9, 2009, at 1:09 AM, Grundy, Jim D wrote:

> 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
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs