An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
Try CVC4 online!
The following sources are partially outdated, but could still
be useful in some cases.
General documentation is available in the CVC4 wiki which includes the CVC4 user manual and