1

I am having some hard time getting the Z3 Python frontend to work on Windows 7 with Z3 version 4.3.0 from codeplex. The older version 4.1.2 that was distributed as an MSI file works fine on my Windows 7.

First, I cannot use the source code from codeplex to build Z3 because I don't have Visual studio Command Prompt (do I really need it?). So I download the binary file 32 bit version and add that directory to my PYTHONPATH. This allows me to do import z3 , but I cannot use it any further because of the error Z3Exception: 'init(Z3_LIBRARY_PATH) must be invoked before using Z3-python' . The file z3.dll is not included in the download file.

I have no problem setting Z3 v4.3 on my Mac or Linux.

Vu Nguyen
  • 987
  • 1
  • 9
  • 20

1 Answers1

2

Visual Studio Express should be enough to compile Z3 and is available for free from Microsoft, here. However, it's not a requirement that Z3 be compiled from scratch to use Z3Py.

Starting with version 4.3.0, the DLL is now called libz3.dll and I just verified that it is indeed included in the download from Codeplex and it executes fine when I add it to PYTHONPATH. I can imagine that what went wrong in your case is that you added the directory C:...\z3-4.3.0-x86 to PYTHONPATH, while it is necessary that C:...\z3-4.3.0-x86\bin be added (note the \bin in the end).

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • hi Chris, actually I did add the \bin directory (that's why I was able to do the import z3 fine). I also tried z3.init("libz3.dll") but I believe there was some error. I don't have access to my Win machine now but I can post the error tomorrow. Does it work for you when you do z3.init("libz3.dll") ? – Vu Nguyen Nov 13 '12 at 21:58
  • Great! Thanks for the information. There is another thing I forgot to mention: It depends on what version of Python is installed; I believe the x64 version also requires that the x64 DLL is used. – Christoph Wintersteiger Nov 14 '12 at 14:34
  • Christoph is correct. If we have Python x64, then we must use the the x64 Z3 DLL. Note that, if we have a 64 bits machine, but we are using a 32-bit Python (very common scenario), then we must use the 32 bits Z3 DLL. – Leonardo de Moura Nov 14 '12 at 17:12