From 698c8ffb48bf01356bda052711bed074662b2401 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 30 Apr 2015 18:21:27 +0200 Subject: More details on the installation of the provers --- INSTALL.md | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/INSTALL.md b/INSTALL.md index 1d0a8df..e384583 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -41,7 +41,28 @@ Currently, these solvers are: Please download the solvers you would like to use via the above links (since SMTCoq might not support later versions), and follow the instructions available for each solver in order to compile them **in a -proof production mode**. +proof production mode**, as detailed below. + + +### veriT + +The +[above link](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz) +points to a snapshot of veriT which is known to be compatible with +SMTCoq, and is already in proof production mode. If you encounter +problems to compile it, please report an issue. + + +### zChaff + +zChaff is not actively maintained, so you might encounter problems to +compile it on modern platforms. +[This patch](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/zchaff64.patch) +might solve your problems (thanks to Sylvain Boulmé for it); if not, +please report an issue. + +To turn proof production on, you need to uncomment the line +`// #define VERIFY_ON ` in `zchaff_solver.cpp`. ## Installation from the sources -- cgit