Boogie's /prover option

May 12, 2011 at 8:59 AM

Hi all,

how is the /prover option of Boogie supposed to be used? I tried

   /prover:"C:\Program Files (x86)\Microsoft Research\Z3-2.15\bin\XXX"

with XXX being z3.dll/lib/exe, just 'z3' and 'Microsoft.Z3.dll', 'Microsoft.Z3', but Boogie always crashes with

   Unhandled Exception: System.IO.FileNotFoundException: Could not load file or assembly 'file:///C:\Pro
   gram Files (x86)\Microsoft Research\Z3-2.15\bin\Microsoft.Z3' or one of its dependencies. The system
   cannot find the file specified.

Regards,
Malte

Coordinator
May 12, 2011 at 5:35 PM

Hi Malte,

The /prover option specifies a DLL that knows how to communicate with the prover at hand.  If you say /prover:Z3 (which is the default), you will be at the mercy of Prover.Z3.dll to find the Z3 executable.  It first looks in the Boogie binaries directory (that is, the directory where Boogie.exe is); failing that, it then looks in the standard places where Z3 installs itself, finding the newest version of Z3 among those places.  There's currently no option to tell Prover.Z3.dll a particular path to the Z3 executable (but if you would like to implement one, such an option would be very welcome).  For now, I guess the best you can do is copy whichever Z3 version you want into the Boogie binaries directory, since Prover.Z3.dll looks there first.

  Rustan

PS.  If you want to see which Z3 executable is being used, call Boogie with the /trace switch.

May 13, 2011 at 8:20 AM

Hi Rustan,

I indeed currently work around this by creating a symlinks in the Boogie binaries directory pointing to the desired Z3.exe's, which makes it somewhat easier to use different Z3 versions by renaming the symlinks, e.g. from Z3v216.exe to Z3.exe, thereby "activating" it.
Anyway, I'll add adding such a cli option to Boogie to my to-do list.

Cheers,
Malte

Jul 5, 2011 at 12:35 PM

Hi all,

one can now specify the Z3 executable to use via -z3exe:"path\to\z3.exe".

Regards,
Malte

Apr 22, 2014 at 5:38 PM
Edited Apr 22, 2014 at 5:39 PM
mschwerhoff wrote:
Hi all, one can now specify the Z3 executable to use via -z3exe:"path\to\z3.exe". Regards,Malte
I still can't get it to work.
C:\Projects\Boogie\Bin>boogie /printInstrumented /z3exe:C:\ProgramFiles\Z3-4.3\bin\z3.exe ..\Test\textbook\Find.bpl
gives:
Unhandled Exception: Microsoft.Boogie.ProverException: Cannot find executable: C:\Projects\Boogie\Bin\z3.exe
at Microsoft.Boogie.SMTLib.Z3.FindExecutable() in c:\boogie\Source\Provers\SMTLib\Z3.cs:line 98
(yes the "ProgramFiles" directory is correct!)

It only works when i copy all the Z3 files into the Boogie\bin directory