在Python 3（Spyder）中安装Z3-solver后无法全局导入的问题

问题描述 #

在Windows 11 64位系统、Python 3.12.1、Spyder编辑器环境下，仅能在Z3发布包自带的..\z3-4.12.4-x64-win\bin\python路径下运行Z3示例代码：

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())

在其他位置运行时，报错：

ModuleNotFoundError: No module named 'z3'

已执行的操作包括：下载Z3 4.12.4解压到Python的site-packages目录、添加Path和PYTHONPATH环境变量、尝试pip安装z3-solver，但问题未解决。

解决方案 #

方法1：修复手动安装的Z3（指定4.12.4版本） #

1. 卸载pip安装的z3-solver，避免版本冲突：

   pip uninstall -y z3-solver
   

2. 打开解压后的Z3目录，找到z3-4.12.4-x64-win\bin\python\z3文件夹（包含__init__.py等核心文件），将这个z3文件夹直接复制到C:\Users\name\AppData\Local\Programs\Python\Python312\Lib\site-packages目录下。
3. 删除之前设置的PYTHONPATH环境变量（或修改为指向包含z3文件夹的目录），Python默认会从site-packages加载模块。
4. 重启Spyder和所有终端窗口，让环境变更生效，再运行测试代码。

方法2：用pip安装指定版本z3-solver（更简便） #

1. 删除手动解压到site-packages的Z3相关文件，避免冲突。
2. 执行命令安装4.12.4版本：

   pip install z3-solver==4.12.4
   

3. 安装完成后直接在Spyder中运行测试代码即可。

关键检查点 #

• 确认Spyder使用的Python解释器为目标版本：打开Spyder，依次点击工具→偏好设置→Python解释器，验证路径为C:\Users\name\AppData\Local\Programs\Python\Python312\python.exe，若不是则切换到该路径。
• 环境变量修改后必须重启所有相关程序，否则变更不会生效。

内容的提问来源于stack exchange，提问作者v2rwbtc6