は場合は、「I「はSMTで再帰関数のためのモデルの検索」のアンドリュー・レイノルズとの共同-authorsによって紙に次の情報を発見した

Question

再帰関数

のための有限モデルの発見モードを有効にする必要があります

CVC4の現在のバージョンをインストールしましたが、--fmf-funはCVC4で利用できませんか？Can（？）あなたはこの中で私を案内してください。

Answer 1

オプション--fmf-funは最新の安定版（1.4）では使用できませんが、最新の開発リリースで利用できます。

最新版のCVC4はhttp://cvc4.cs.nyu.edu/downloads/（ページの右側にあります）からダウンロードできます。