SMTLib compliance: -7.0 is a valid identifier.

[LeventErkok]

Strictly speaking, the following is a valid SMTLib2 benchmark:

(set-option :produce-models true)
(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-fun -7.0 () Int)
(assert (= -7.0 0))
(check-sat)
(get-model)

And it's accepted by CVC4, Yices, and MathSAT just fine. But z3 complains:

(error "line 4 column 13: invalid function declaration, symbol expected")

Just dropping this here as a note; I think this is one place where diverging from the standard is probably the right choice. But the presence of the directive (set-option :smtlib2_compliant true) makes this harder to swallow.