z3 (Microsoft Research) Web サイトで提供されている MaxSAT/MaxSMT c の例 (具体的には maxsat.c) をいじってみたいと思っています。Visual Studio 2010 を使用して、最終的にコンパイルするサンプルを取得しました (z3 4.0 の新規インストールを使用)。しかし、それらを使用して (SMT 2.0) モデルを実行することはできません。さらに、この質問に投稿された例も機能しません。
最初のケースでは、コンパイルしたプログラムがファイルを呼び出そうとするとクラッシュしZ3_get_smtlib_num_formulasますget_hard_constraints。代わりに、標準の Windows 7 の「このプログラムは動作を停止しました」というポップアップが表示される理由はわかりません。
2 番目のケースでは、レポートしますunsupported ;benchmark。
この作業を手伝うために、(a) このコードをコンパイルするときに同様の問題が発生した人はいますか? もしそうなら、どのように解決しましたか? または（b）ファイルのコンパイルをデバッグするにはどうすればよいですか（正しいと仮定して）？つまり、誰かが正しいライブラリ (およびライブラリのバージョン - z3 4.0 など) を列挙して、この例を機能させるためにコンパイラ オプションに含めることができますか?
どちらの場合でも、2 番目のケースで報告されたエラーに関する情報も歓迎されます。それは正確にはどういう意味ですか? キーワードが無効でしたか? SMT 入力のバージョンが間違っていますか? または、他の何か？
ありがとう。