It seems that define-funs-rec
is a strict superset of what define-fun
can do according to the SMTLIB standard. If so is there a reason for not always using define-funs-rec
, maybe except for syntactic simplicity?
Strictly speaking; no. But define-fun-rec
is rather new (as opposed to good old define-fun
), so if you want greater portability and have no need for a recursive definition, then you should stick to define-fun
.
It is conceivable that the define-fun-rec
might also bring heavier-machinery in a solver that is not really needed unless you really have a recursive definition, such as a well-foundedness checker. This might end up costing some performance cycles; though I doubt this would be too much of a concern.