Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Windows: Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")

Tags:

python

z3

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

like image 296
ZhouW Avatar asked Sep 02 '17 03:09

ZhouW


1 Answers

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.

like image 77
Nikolaj Bjorner Avatar answered Oct 21 '22 07:10

Nikolaj Bjorner