A Tutorial for Running Boogie and Z3 on Linux

Share

I just learned that Boogie recently switched to using .NET 4, and therefore the tutorial on how to run Boogie under Linux using .NET 2 I wrote a couple of months ago is now deprecated. I played a little bit with the latest version of Boogie under Linux and managed to get it to work, this time using Mono.

So, first you have to get a Linux binary of Z3. You can always download the latest SMT Competition Z3 Linux binary from the Z3’s download page (look for Other platforms). Copy the bin/z3 executable into Boogie’s folder and rename it to z3.exe.

Alternatively, you can try to get the Windows Z3 binary to work under Linux using wine. So, to be able to run z3.exe, install wine (I am using wine-1.1.28) and download the winetricks script (I am using winetricks version 20090815). Then, using winetricks install vcrun2008

winetricks vcrun2008

Now try typing

wine z3.exe /h

to see if Z3 is working. For Boogie to be able to call Z3, you still have to achieve that z3.exe can be executed without the wine command in front. This is the tricky part that is accomplished using binfmt_misc and doing the following:

su
mount binfmt_misc -t binfmt_misc /proc/sys/fs/binfmt_misc
echo ':DOSWin:M::MZ::/usr/bin/wine:' > /proc/sys/fs/binfmt_misc/register

Try calling Z3 without wine

z3.exe /h

to see if Z3 is still working.

Second, install the latest version of Mono that supports .NET 4. Boogie is going to fail if the environment variable ProgramFiles is not set, but you can fool it by setting ProgramFiles to essentially anything:

export ProgramFiles=/home/

Create a simple bpl file test.bpl and check if just Boogie without Z3 is working using Mono:

mono --runtime=v4.0.30319 Boogie.exe test.bpl /noVerify

Finally, check if Boogie/Z3 combination is working together and execute:

mono --runtime=v4.0.30319 Boogie.exe test.bpl

You can also get rid of the ugly –runtime switch, if you edit Boogie.exe.config like this:

<?xml version="1.0"?>
<configuration>
  <startup>
    <supportedRuntime version="v4.0.30319" sku=".NETFramework,Version=v4.0"/>
  </startup>
</configuration>

And voila, you are done!
I would like to thank Vladimir Klebanov for his valuable feedback and help, and any additional feedback, comments, or improvements would be appreciated.

You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.

Comments are closed.