Tom
Tom

Reputation: 934

For handling recursive function definition in CVC4 need to enable finite model finding mode for recursive functions

I have found the following information in paper by Andrew Reynolds and co -authors "Model Finding for Recursive Functions in SMT"

"If CVC4’s finite model finding mode for recursive functions is enabled (using the command-line option --fmf-fun)"

But I have install current version of CVC4, --fmf-fun is not available in CVC4?Can you please guide me in this.

Upvotes: 0

Views: 145

Answers (1)

Andrew Reynolds
Andrew Reynolds

Reputation: 36

The option --fmf-fun is not available in the latest stable release (1.4), however, it is available in the latest development release.

You can download the latest development version of CVC4 at http://cvc4.cs.nyu.edu/downloads/ (on the right of the page).

Upvotes: 2

Related Questions