This project is read-only.

How to install and build the sources using Mono

Boogie can be built and run on Mac OS X and Linux machines following the instructions below.


Building from command line

Go to the Sources directory and use the xbuild command to build the Boogie.sln solution.
$ cd /path/to/boogie/Source

# Restore the NuGet packages used by Boogie
$ wget
$ mono ./nuget.exe restore Boogie.sln

# Build Boogie
$ xbuild Boogie.sln

# Run unit tests (replace "Release" with the build type of Boogie)
$ UnitTests/ Release

Building in Monodevelop

  1. Start Monodevelop
  2. If you don't have the NuGet add-in installed then install it ( Tools > Add-in Manager )
  3. Open Source/Boogie.sln and select Build > Build All from the menu
  4. Run the unit tests by going to the Unit Tests panel and clicking on Run All

Note that projects other than Boogie itself (i.e. Dafny, Chalice, BCT) have not yet been tested under Mono.


Boogie will try to find Z3 in its Binaries directory, named z3.exe. You can make this available by creating a symlink as below:
ln -s /path/to/z3/bin/z3 /path/to/boogie/Binaries/z3.exe

Now you can run Boogie using mono:
mono /path/to/boogie/Binaries/Boogie.exe input.bpl

You may wish to create an alias for easy access in your .bashrc or similar:
alias boogie='mono /path/to/boogie/Binaries/Boogie.exe'

Running the driver test suite

To make sure your build of Boogie is working correctly you should run the driver test suite. See here for details.

Last edited Nov 17, 2014 at 9:40 PM by danliew, version 6


kenmcmil Feb 18, 2014 at 9:32 PM 
This doesn't work with Mono 3.2.1 under Ubuntu because Boogie specifies the Client Profile, which mono doesn't have. You need the option /tv:4.0 on the xbuild command line. Also, monodevelop doesn't like the solution file Boogie.sln because the VS version number is 12.0. Change it to 11.0 and monodevelop will be happy.

danliew Jan 15, 2014 at 2:44 PM 
The path is slightly wrong is should be




colinadams Feb 9, 2013 at 8:20 PM 
The link for the Z3 download:
does not exisy