Skip to content
solver for the reachability modulo theories problem
Branch: master
Clone or download
Latest commit 0e6ae9b Mar 14, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
boogie @ 6ecd6bb
tools Added the concurrency explorer tool Nov 27, 2017
.gitmodules added boogie git submodule May 20, 2016
LICENSE.txt Update LICENSE.txt Apr 16, 2016 Updated README Jun 25, 2016
app.config Dual houdini Oct 10, 2015


Corral is a solver for the reachability modulo theories problem. Learn more here:

Dependency on Boogie

Corral has a dependency on Boogie, which is provided as a git submodule. To download the specific revision of Boogie that Corral depends on:

git submodule init
git submodule update
cd boogie

Building and running Corral on Windows

Here is how you set up Corral.

  1. Build cba.sln. This solution includes the necessary Boogie projects; there is no longer a separate step to build Boogie.
  2. Running Corral requires z3. We have tested Corral against z3 version 4.1; download and copy z3.exe in bin\debug folder, alongside the corral.exe executable.
  3. Corral takes a Boogie program as input. There are regressions provided in test\regressions folder. Go to this folder and run perl to run all the regressions. You can run an individual test, for instance, as follows: go to test\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 file filename.

Building and Running Corral on Linux using Mono

The following worked for Matt McCutchen on Fedora 23. You may need to change the TargetFrameworkVersion to match what your Mono version provides.

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 ...
You can’t perform that action at this time.