Installation problem

Sep 13, 2011 at 3:00 PM
Edited Sep 14, 2011 at 12:05 PM

Hello, I've installed Z3 and extracted the Boogie-zip-file. When I run Dafny on an example file, I get

~$ /cygdrive/c/Program\ Files/Microsoft\ Research/boogie/Dafny.exe test.dfy

Unhandled Exception: System.IO.FileLoadException: Could not load file or assembly 'file:///C:\Progra
m Files\Microsoft Research\boogie\Provers.Z3.dll' or one of its dependencies. Operation is not suppo
rted. (Exception from HRESULT: 0x80131515) ---> System.NotSupportedException: An attempt was made to
 load an assembly from a network location which would have caused the assembly to be sandboxed in pr
evious versions of the .NET Framework. This release of the .NET Framework does not enable CAS policy
 by default, so this load may be dangerous. If this load is not intended to sandbox the assembly, pl
ease enable the loadFromRemoteSources switch. See http://go.microsoft.com/fwlink/?LinkId=155569 for
more information.

However, Provers.Z3.dll exists at the specified location and I have read an execute permissions. I use .NET 4.

Nov 8, 2011 at 1:51 AM

Windows remembers that this DLL came from (a ZIP file that came from) the Internet.  Therefore, it blocks you from running it.  You need to unblock it.

So, why is the complaint about Prover.Z3.dll and not, say, Boogie.exe or Dafny.exe, since they also came from the Internet.  My guess is that when you explicitly run an executable, you are telling Windows that you're okay with overriding the blocking for that executable and its linked DLLs (like Core.dll).  However, Prover.Z3.dll is loaded dynamically by Boogie, so I'm guessing that's why the blocking comes into play.

The solution is simple:  Right-click on the file (Prover.Z3.dll) and select Properties.  Then, click the "Unblock" button at the bottom of the properties dialog and click OK.

If you get this complaint for other DLLs, you'd have to do it from them too, but you can do it all in one go:  After you download the ZIP file with all the binaries, right-click on it, select Properties, click Unblock, and click OK.  That will mark the entire ZIP file, so when you then unzip it, the files in it will all be marked as unblocked.

Btw, note that this issue arises only when you download the binary distribution.  If you build from sources, Windows treats the resulting binaries as coming from your machine (since you built them).

  Rustan

Nov 9, 2011 at 11:28 AM

Thanks, it works now.

Mar 11, 2012 at 1:59 PM

I had a similar problem. It turned out to be down to the fact that the Boogie/ directory was placed on a network drive. When I moved it back to C:/, things worked fine.