z3 - Z3 支持 -m 选项

Question

在 unix 上，我正在尝试使用使用 Z3 的 AProVE。我下载并构建了源代码（4.1.2；虽然 z3 -version 显示 4.2）。AProVE 使用带有 -m 选项的 z3，但 4.2 不支持 -m。根据 AProVE 开发人员的说法，-m 在 z3 4.0 中可用。

如何获取支持 -m 的 z3 的源文件？或者，我的问题有简单的解决方法吗？

Answer 1

默认情况下启用模型生成。我们不再需要提供选项-m。如果您无法更改 AProVE，您可以为 Z3 创建一个包装器，-m在调用 Z3 之前删除该选项。另一种选择是破解shell\main.cppZ3 源代码中的文件。它包含一个名为

void parse_cmd_line_args(int argc, char ** argv)

-m要包含一个不执行任何操作的虚拟选项，您只需包含一个新的if-statement.

        else if (strcmp(opt_name, "m") == 0) {
            // do nothing
        }