Z3 Int 未定义错误答案

【问题标题】：Z3 Int not defined errorZ3 Int 未定义错误
【发布时间】：2016-06-28 04:22:09
【问题描述】：

我正在尝试使用 python 中的 Z3 库，但它不起作用。它给出了一个错误 Int is not defined.

我使用 pip 安装了 z3 模块，如您所见，当我导入 lib 时没有抛出错误消息。我正在使用 Mac OS X 和 python 版本 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

【问题讨论】：

标签： python z3

【解决方案1】：

一开始我也有同样的问题。

问题的原因是你没有安装正确的包。

正确的包名是z3-solver。

要安装它：

pip install z3-solver

【讨论】：