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

Answer 1

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