z3 - 我可以从 Pex 获取 SMT 2 格式的路径条件吗？

Question

我正在使用 z3_logdir 和 z3_loglevel 环境变量使 Pex 以 *.z3 文件格式记录路径条件。有没有办法强制 pex 以 SMT 2 格式导出路径条件？或将 .Z3 文件格式转换为 SMT 2 ？

Answer 1

Pex 附带 Z3 的 DLL：Microsoft.Z3.dll。这对应于 Z3 版本 2.5（可以从http://research.microsoft.com/en-us/um/redmond/projects/z3/old/older_z3.html下载）。Z3 v 2.5 中的 API 包含将 Z3 文件解析为内部格式的支持，并且有用于将这些文件转储到 SMT-LIB(1) 的 API 函数。更新版本的 Z3 和其他工具可用于将 SMT-LIB1 基准转换为 SMT-LIB2。