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
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:
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
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:
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:
<supportedRuntime version="v4.0.30319" sku=".NETFramework,Version=v4.0"/>
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.