小编Aka*_*yas的帖子

我无法让任何 z3py 示例正常工作。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了 python 路径以指向适当的目录。此外，我能够成功导入 z3，但每次声明变量时都会出现错误。编译器无法识别 Int、Ints、Real 和 RealVal。

我举了一个例子来说明。

代码：

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

错误：回溯（最近一次调用）：文件“test.py”，第 3 行，在 x = Int('x') 中 NameError: 名称 'Int' 未定义

我真的很感激任何帮助。太感谢了。