z3 - -m オプションの Z3 サポート

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 用のラッパーを作成できます。もう 1 つのオプションはshell\main.cpp、Z3 ソース コード内のファイルをハッキングすることです。と呼ばれる機能が含まれています。

void parse_cmd_line_args(int argc, char ** argv)

-m何もしないダミーのオプションを含めるには、 new を含めるだけif-statementです。

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