dargones / corral

solver for the reachability modulo theories problem

Corral

Corral is a solver for the reachability modulo theories problem. Learn more here: http://research.microsoft.com/en-us/projects/verifierq

Building and Running Corral

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

SMT Solver

Running Corral requires Z3. We have tested Corral against Z3 version 4.8.8.

Regressions

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.

Versioning and Release

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.