Corral is a solver for the reachability modulo theories problem. Learn more here: http://research.microsoft.com/en-us/projects/verifierq
You can build Corral using .NET Core:
$ dotnet build source/Corral.sln
Then you can run the generated executable:
$ source/Corral/bin/Debug/net5.0/corral ...
Alternatively, Corral can be installed as a .NET Core Global Tool:
$ dotnet tool install --global Corral
Running Corral requires Z3. We have tested Corral against Z3 version 4.8.8.
Corral takes a Boogie program as input. There are regressions provided in
test\regressions
folder. Go to this folder and run perl check.pl
to run all
the regressions. You can run an individual test, for instance, as follows: go to
test\regressions
and do: ${CORRAL_EXE} 001\001.bpl /flags:001\config
. The flag /flags:filename
instructs corral to read its
flags from the file filename
.
To push a new version to nuget, publish a new release with a tag of the form
vx.y.z
, where x.y.z
is the updated version.
The release workflow will automatically build and push the packages.