[SMT-LIB] Response to (exit) Command?

[Tjark Weber]

May (must?) a compliant solver issue a "success" response to the (exit)
command?

Figure 3.10 in the SMT-LIB Standard is inconclusive, as the script
contains a previous "(set-option :print-success false)" command.

Section 4.1.2 states
| The value success is the default response for a successful execution
| of a supported command.

In my opinion this is ambiguous. Arguably, when the (exit) command has
been successfully executed (and not just parsed), the solver is no
longer able to respond at all.

It is perhaps unsurprising then that different SMT solvers currently
show different behavior. (veriT seems to print "success", while most if
not all other solvers don't.)

I would suggest to add a clarifying remark or footnote to the Standard,
perhaps in Section 4.2.1, that details which behavior(s) are required
or permitted here.

Best,
Tjark