This page gives a few tips to download, install and/or configure external provers.

Automatic provers

Simplify (at least version 1.5.4): is available under binary form for various architectures from this page or directly here
Alt-Ergo (at least version 0.8): is available under binary form for Unix, or under source form to be compiled using the OCaml compiler, from this page. A Microsoft Windows installer (for version 0.7.3) is also available on this page
Z3 (at least version 1.3):
- Microsoft Windows version: is available from this page.
- Native Linux/x86 version.
  A linux version of Z3 (version 2.2) is provided by courtesy of the authors. It is distributed here as is, under the same license as the Windows Version which can be found here
- Running Windows version under Wine layer
  Running the MS Windows version of Z3 under Unix is also possible via the wine layer: install z3 using the msiexec command and then run it using this script where you have to modify the full path to z3.exe
  See also this page for hints on running Z3 under Unix or Mac OS X
Yices (at least version 1.0.17): available under binary form for various platform from this page. (Note that Yices version 2 which participated to the SMT-COMP 2009 has no support for quantifiers; thus you should not use it with Why.)
CVC3 (at least version 1.5): available under source form and as a Linux binary from this page
Gappa (at least version 0.12.0): available under source form at this page

Proof assistants