35

I am running into the following error when using a python script (oyente) that uses Z3 (which I've built in the Visual Studio command prompt):

File "C:\Python27\Lib\site-packages\oyente\z3\z3core.py", line 23, in lib
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3.z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.__del__ of <z3.z3.Context instance at 0x0000000003A5AC48>> ignored

I have the libz3.dll file in the z3 and oyente directory, and in my PYTHONPATH in system variables I have added every directory that might possibly need to be there, eg:

enter image description here

ZhouW
  • 1,187
  • 3
  • 16
  • 39

2 Answers2

1

This is a common error when invoking a 32 bit version of Z3 from a 64 bit version of python or the other way around.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • 1
    I'm using the 64 bit version of python (verified by `import platform` and `platform.architecture()[0]` in the python console) and have tried using the 64 bit version of z3 for windows at https://github.com/Z3Prover/z3/releases/tag/z3-4.5.0 (instead of downloading the source code and compiling). I have added "C:\Python27\Lib\site-packages\oyente\z3-4.5.0-x64-win\bin" (which contains libz3.dll) to my PYTHONPATH system variable and still get the same error. – ZhouW Sep 02 '17 at 05:25
  • 1
    Did you add that path to your PATH as well? (The system needs to see the .dll; Python needs to see the .py files.) – Christoph Wintersteiger Sep 07 '17 at 13:31
0

Have you seen Installing Z3 + Python on Windows? As Nikolaj pointed, seems to be a 32/64 bit confusion, either in Z3 or Python or your machine itself.

alias
  • 28,120
  • 2
  • 23
  • 40