Installation Instructions - lgwagner/SpeAR GitHub Wiki
The installation instructions in this section assume a Windows environment.
Download SpeAR from https://github.com/lgwagner/SpeAR/releases. Extract the zip file to a location of your choice (e.g., C:\spear_win64_rc20).
To run realizability analysis in SpeAR, you will need to install Z3, available at https://github.com/Z3Prover/z3/releases.
Download the zip file and extract the files to a location of your choice.
Add a user environment variable Z3_HOME whose value is the path to the folder with the Z3 files (e.g., C:\z3-4.5.0-x64-win). Then add %Z3_HOME%\bin to the PATH user environment variable (if needed, add the PATH user environment variable).
In order to use SpeAR’s graphical view generation capability, you will need to install Graphviz, available at http://graphviz.org/Download.php.
After reading the license and clicking "Agree," you will be presented with several download options. For Windows, click "Stable and development Windows Install packages."
Either run the *.msi file or extract the zip files to a location of your choice.
Add the path to the Graphviz bin folder (e.g., C:\Program Files (x86)\Graphviz2.38\bin) to the Path system environment variable.
To confirm that Graphviz is installed and can be found by the system, type dot –V at a command prompt. The user should get a response with the graphviz version number as shown below.
C:\>dot -V <br/> dot - graphviz version 2.38.0 (20140413.2041)
Troubleshooting note: Some users found they needed to ‘Repair’ the Graphviz installation via Windows "Uninstall or change a program" before the system could find Graphviz, even though the Graphviz bin folder was on the path.
Open SpeAR (<path></path>\eclipse-spear\spear.exe). (We recommend pinning a shortcut to the Start menu first.)
Create or select a workspace (e.g., C:\spear_workspace).
Once the workspace is open, select Z3 as the SMT Solver by going to Window -> Preferences -> Spear -> Analysis and selecting Z3 from the drop down menu next to "SMT Solver." Also, set the number of PDR instances to 1. (If your computer has more than four cores, you may set the number of PDR instances to four less than the number of cores.)
If Z3 was installed properly, it should be listed as a detected solver when “Check if available” is clicked.
