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

[Tinelli, Cesare]

Tjark,

On 28 Jun 2015, at 11:10, Tjark Weber <tjark.weber at it.uu.se> wrote:

> Cesare,
> 
[...]
>> The real question is perhaps what it means to successfully execute
>> 'exit'. In my view, it means to be able to release all resources and
>> quit. So printing 'success' on the standard output would be the very
>> last operation before quitting.
> 
> Being able to release all resources and quit is different from actually
> releasing all resources and quitting. The (exit) command should trigger
> the latter. Therefore, I think one could argue that (exit) hasn't been
> successfully executed until after the solver has quit (at which point
> the solver no longer can print anything).
> 
Fair enough, in that case I would go with option (2) below.

I'd like to hear from more people though.


Cesare


>> I can sure add a clarification now, but we could also take the opportunity to discuss explicitly first whether the standard should:
>> 
>> 1) require 'exit' to print 'success',
>> 2) require 'exit' not to print anything, or
>> 3) allow it to print 'success' without requiring it
>> 
>> The status quo among solvers is best reflected by option 3, but I would be against it and would settle on either 1 or 2.
> 
> I agree, and I have no strong preference between 1) and 2). As
> mentioned, most solvers currently do not print success.
> 
> Best,
> Tjark
> 
>