Reputation: 934
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
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