Corral is a solver for the reachability modulo theories problem. Learn more here: https://research.microsoft.com/en-us/projects/verifierq
Corral has a dependency on Boogie, which is provided as a git submodule. To download the specific revision of Boogie that Corral depends on:
cd ${CORRAL_DIR}
git submodule init
git submodule update
cd boogie
Here is how you set up Corral.
- Build
cba.sln
. This solution includes the necessary Boogie projects; there is no longer a separate step to build Boogie. - Running Corral requires z3. We have tested Corral against z3 version 4.1; download and copy z3.exe in
bin\debug
folder, alongside thecorral.exe
executable. - Corral takes a Boogie program as input. There are regressions provided in
test\regressions
folder. Go to this folder and runperl check.pl
to run all the regressions. You can run an individual test, for instance, as follows: go totest\regressions
and do:..\..\bin\debug\corral.exe 001\001.bpl /flags:001\config
. The flag/flags:filename
instructs corral to read its flags from the filefilename
.
The following worked for Matt McCutchen on Fedora 23. You may need to change the TargetFrameworkVersion
to match what your Mono version provides.
cd ${CORRAL_DIR}
xbuild /p:TargetFrameworkVersion=v4.5 /p:Configuration=Debug cba.sln
ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe
mono bin/Debug/corral.exe ...