Z3 ist ein SMT-Löser, d.h. er kann SAT-Formeln bezüglich verschiedener Theorien lösen. Als Eingabesprache verwendet Z3 den SMT-LIB 2.0 standard.
/opt/provers/z3/bin/z3
/opt/provers/cvc4/bin/cvc4
contrib/get-antlr-3.4
./configure –prefix <Zielpfad>
make
und im Zielverzeichnis installieren make install
/opt/provers/yices/bin/yices
(Yices-Sprache)/opt/provers/yices/bin/yices-smt
(SMT-LIB 1.0)/opt/provers/yices/bin/yices-smt2
(SMT-LIB 2.0)/opt/provers/yices/bin/yices-sat
(DIMACS-Format)./install-yices <Installationsverzeichnis>
ausführen/opt/provers/mathsat/bin/mathsat