Z3 Int not defined error

Question

I am trying to use Z3 library from python however it does not work. It gives an error Int is not defined.

I installed the z3 module using pip and as you can see, there is no error message thrown when I import the lib. I am using Mac OS X and python version 2.7.6

>>> from z3 import *
>>> x = Int('x')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'Int' is not defined

z3 appears to be an interface to a C++ library - have you installed the library it's trying to use? github.com/Z3Prover/z3 has instructions — Simon Fraser
Did you install the package called angr-z3 or a different one? — Christoph Wintersteiger

Cpp Forever Cpp Forever · Accepted Answer · 2019-09-10T08:34:40

I have the same problem at the beginning.

The cause of the problem is that you didn't install the right package.

The right package name is z3-solver.

To install it:

pip install z3-solver

Z3 Int not defined error

1 Answers