[SMT-LIB] Issues with define-fun for Functions of Arity 0

[Tjark Weber]

On Thu, 2016-04-21 at 15:48 +0200, Tjark Weber wrote:
> Moreover, there are currently numerous SMT-LIB benchmarks in
> *quantifier-free* logics that use define-fun to define functions of
> arity 0.

Further analysis of the 2015-06-01 SMT-LIB release also revealed
numerous benchmarks that are classified as quantifier-free but use
'define-fun' to define functions of arity >= 1.

Perhaps those benchmarks should be re-classified?

Best,
Tjark