VeriEQL适配Z3版本咨询、安装报错及版本查看方法求助

问题详情 #

• 运行环境：Ubuntu + Python 3.10
• 操作：部署VeriEQL并执行python __main__.py
• 报错：

File "/mnt/compression/VeriEQL/constants.py", line 33, in <lambda>
    And = lambda *args: Z3_And(*args, ctx=Z3_CONTEXT)
TypeError: And() got an unexpected keyword argument 'ctx'

• 已尝试的z3-solver版本：
  • z3-solver-4.5.1.0
  • z3-solver-4.11.2.0
  • z3-solver-4.8.12.0
  • z3-solver-4.15.0.0

解决步骤 #

1. 打印当前加载的Z3版本 #

在__main__.py文件开头添加以下代码，运行后即可看到实际生效的Z3版本：

import z3
print("Loaded Z3 version:", z3.get_version_string())

同时可以在终端执行以下命令，确认pip安装的版本与加载版本是否一致：

pip list | grep z3-solver
python -c "import z3; print(z3.get_version_string())"

如果版本不一致，大概率是系统存在多个Z3安装（比如apt安装的libz3-dev），建议创建虚拟环境重新安装依赖。

2. 适配Z3版本 #

从报错逻辑看，VeriEQL的代码是基于旧版Z3 API编写的，旧版Z3允许显式传递ctx参数，而新版Z3（4.10+）已移除该参数的显式传递方式。

方案一：修改代码适配新版Z3

直接修改constants.py第33行的代码，去掉ctx参数：

And = lambda *args: Z3_And(*args)

如果项目中依赖Z3_CONTEXT上下文，也可以改为绑定上下文的调用方式：

And = Z3_CONTEXT.And

方案二：安装适配的旧版Z3

查看VeriEQL仓库历史提交可知，该项目最初适配的是Z3 4.8.7版本，执行以下命令安装：

pip install z3-solver==4.8.7.0

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