我有兴趣使用 z3（Microsoft Research）网站上提供的 MaxSAT/MaxSMT c 示例（特别是 maxsat.c）。使用 Visual Studio 2010，我最终编译了示例（使用全新安装的 z3 4.0）。但是，我无法让我的任何（SMT 2.0）模型使用它们来运行。此外，我也无法让这个问题中发布的示例正常工作。
Z3_get_smtlib_num_formulas在第一种情况下，我编译的程序在尝试调用get_hard_constraints文件时崩溃。我不知道为什么，相反，我得到标准的 Windows 7“这个程序已停止工作”弹出窗口。
在第二种情况下，它报告unsupported ;benchmark.
为了帮助我完成这项工作，我想知道（a）是否有人在编译此代码时遇到过类似的问题，如果有，您是如何解决的？或（b）如何调试文件的任一编译（假设它是正确的）？即，有人可以枚举正确的库（和库版本 - 例如，z3 4.0？）以包含在编译器选项中以使此示例正常工作吗？
在任何一种情况下，关于第二种情况下报告的错误的信息也将不胜感激：这到底是什么意思？关键字无效？那SMT输入是错误的版本？或者是其他东西？
谢谢。