User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools



This shows you the differences between two versions of the page.

Link to this comparison view

mantis:frama-c:faq [2012/05/16 15:57]
yakobowski created by moving content from main page
mantis:frama-c:faq [2013/05/21 17:01] (current)
bobot update provers installation tips (thx alain giorgetti)
Line 43: Line 43:
 ==== Installing theorem provers ==== ==== Installing theorem provers ====
-A few tips for installing provers are provided on [[​provers.html|Why's page]].\\ Here are detailed instructions for making use of Z3 on Ubuntu x86+Links for installing provers are provided on [[|Why3's page]].\\ Here are detailed instructions for making use of Z3: 
-    - download z3-1.3.6.msi Latest version:​\\ ​[[​details/​0a7db466-c2d7-4c51-8246-07e25900c7e7/​details.aspx|Z3 1.3]] Safari users: use Firefox to download if it looks like the server is down (it probably isn't, just incompatible). +  * go to [[​README|Z3 source homepage]] 
-    - open with wine or msiexec and install +  * Click on the 'Download' ​button 
-    - create your ''​$HOME/​bin'' ​directory +  * Save the zip in a local folder, say z3-sources/. 
-    ​- ​in your ''​.bashrc''​ add:\\ ''​export PATH=$HOME/​bin:​$PATH''​ +  * Run the following commands:
-    - restart session +
-    - in ''​$HOME/​bin''​ add file z3  with content\\ ''​args=`echo $* | sed -e '​s|/​|\\\|g'​`''​ \\ ''​exec wine $HOME/.wine/​drive_c/​Program_Files/​Microsoft_Research/​Z3-1.3.6/​bin/​z3.exe /s $args''​ +
-    - save and change permission:\\ ''​sudo chmod 775 z3''​ +
-    - Run ''​why-config''​+
 <​code>​ <​code>​
-starting autodetection... +cd z3-sources 
-Found prover Alt-Ergo version 0.8 +unzip z3[tab for completion] 
-Found prover ​Simplify ​version 1.5.+cd z3[tab for completion] 
-err:​winedevice:​ServiceMain driver L"​vstor2-ws60"​ failed to load +autoconf 
-Found prover Z3 version ​1.3 +./​configure 
-Found prover ​Yices version ​1.0.21 +python scripts/​ 
-Found prover ​CVC3 version ​devel +cd build 
-Found prover Coq version ​8.1pl3 +make 
-detection done+sudo make install 
-writing rc file...+</​code>​ 
 +  * z3 executable is installed at /usr/bin, libraries at /usr/lib, and include files at /​usr/​include. 
 +  * Run ''​why3config --detect''​ (the provers, the versions and the plugins detected can be differrent) 
 +Found prover Alt-Ergo version 0.95.1, Ok. 
 +Found prover ​CVC3 version ​2.4.1, Ok. 
 +Found prover Spass version 3.7, Ok
 +Found prover Z3 version ​4.3.1, Ok. 
 +Found prover ​Coq version ​8.4pl1, Ok
 +Warning: ​prover ​Gappa version ​0.17.1 is not known to be supported, use it at your own risk! 
 +5 provers detected and 1 provers detected with unsupported ​version 
 +== Found [..]/​why3/​lib/​why3/​plugins/​hypothesis_selection.cmxs == 
 +== Found [..]/​why3/​lib/​why3/​plugins/​tptp.cmxs == 
 +== Found [..]/​why3/​lib/​why3/​plugins/​dimacs.cmxs == 
 +== Found [..]/​why3/​lib/​why3/​plugins/​genequlin.cmxs == 
 +Save config to ~/.why3.conf
 </​code>​ </​code>​
mantis/frama-c/faq.txt · Last modified: 2013/05/21 17:01 by bobot