[SMT-LIB] concrete syntax of 'success'

[Tinelli, Cesare]

Hi David,

On 17 May 2013, at 02:53, cok at frontiernet.net wrote:

> The SMTLIBv2 standard is clear in its informal text that setting the :print-success option to false suppresses printing 'success' when that would be the result of a command that would respond with 'success'.
> 
> However, the definition of <gen_response> in the concrete syntax does not allow for this. it says that the response is unsupported |  success |  ( error <string> )
> I think that this definition needs to be expanded to allow an empty response, and that the mapping of the abstract syntax 'success' is to either concrete 'success' or empty.
> 
Thanks for pointing this out. We will fix it in the next release.


Cesare


> - David
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib