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

[Tjark Weber]

According to Section 4.2.3 of the SMT-LIB Standard (version 2.5),

  (define-fun f ((x1 σ1) ··· (xn σn)) σ t)

with n ≥ 0 is semantically equivalent to

  (declare-fun f (σ1 ··· σn) σ)
  (assert (forall ((x1 σ1) ··· (xn σn)) (= (f x1 ··· xn) t))

Here, n=0 is explicitly permitted.

However, the grammar for terms in Section 3.6 requires that a "forall"
binder is followed by *one or more* (cf. Section 1.1.3) sorted
variables.

Moreover, there are currently numerous SMT-LIB benchmarks in
*quantifier-free* logics that use define-fun to define functions of
arity 0.

I believe a clarification (probably by providing a special-cased
semantics for n=0 in Section 4.2.3) might be in order.

Best,
Tjark