Project

Profile

Help

HostedRedmine.com has moved to the Planio platform. All logins and passwords remained the same. All users will be able to login and use Redmine just as before. *Read more...*

Bug #180913

open

inconsistency with :print-success option

Added by Cesare Tinelli over 9 years ago.

Status:
New
Priority:
Normal
Start date:
2013-05-26
Due date:
% Done:

0%

Estimated time:

Description

Problem pointed out by David Cok.

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

No data to display

Also available in: Atom PDF