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

[Jochen Hoenicke]

Hello,

2015-06-28 8:51 GMT+02:00 Tinelli, Cesare <cesare-tinelli at uiowa.edu>:

> 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.
>

We prefer option 2, which is what our solver currently implements.  The
reason was given by Tjark: for option 1 we would need to print "success"
before calling exit(), which means we would be lying.  If exit() throws an
exception (which is possible in Java) the error message would be printed
after success.

  Jochen & Jürgen

-- 
Jochen Hoenicke,
Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243