Z3支持-m选项

Question

关于unix，我试图使用AProVE，它使用Z3。我下载并构建了源代码（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创建一个包装，在调用Z3之前删除选项-m。另一种选择是在Z3源代码中破解文件shell\main.cpp。 它包含一个名为

void parse_cmd_line_args(int argc, char ** argv) 

要包括虚拟-m选项，不会做任何事情的功能，你只需要包含一个新if-statement。

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