Recursive Function usage leads to unknown sat (Bugzilla #684)

[mpreiner]

Imported from Bugzilla
Reporter: Holger Vornholt
Status: RESOLVED
Severity: enhancement
Assigned to: Andrew Reynolds
Component: Quantifiers
Milestone: ---
Version: master
Platform: PC
OS: Windows

Original attachment names and IDs:

• recursiveUnknownError.txt (Test script, ID 326)

On 2015-10-12 04:18:40 -0700, Holger Vornholt wrote:

Created attachment 326
Test script

Hi,

trying out recursive functions I discovered that defining a recursive function at all, leads to the satisfiability result being unknown. This behaviour is confusing to me as I did not even assert a constraint that uses the function. It might be correct however. I am not an expert in SMT.

Attached is the used script.

I am starting cvc4 with the command line:
cvc4 --lang smt --string-exp

Version: cvc4 1.5-prerelease [subversion URL: https://github.com/CVC4/CVC4/trunk r4363 (with modifications)]
I am using the nightly build of 10.10.2015 as the newest build is not available yet.

I remember reading that recursive functions lead to quantifiers so I classified this as a quantifier error.

Kind regards,
Holger Vornholt

On 2015-10-15 12:02:39 -0700, Andrew Reynolds wrote:

Hi Holger,
As we discussed, this problem can be solved "sat" by invoking the --fmf-fun option of CVC4.
I will go ahead close this bug.
Cheers,
Andrew