[SMT-LIB] prompts

cok at frontiernet.net cok at frontiernet.net
Fri Jun 26 21:42:59 EDT 2015


The SMT-LIB standard makes a distinction between the regular-output-channel and the diagnostic-output-channel. The former is supposed to contain only S-expressions in the form specified as responses to the various SMT-LIB commands. The latter can contain anything.
What about prompts issued as part of running a solver in interactive mode?Nearly all solvers emit them on the regular-output-channel.Does the standard intend to require that prompts be issued on the diagnostic-output-channel? or is this output allowed on the regular-output-channel.
One more thing to clarify in the standard (that I did not think of in all my reading of it before, until I encountered a solver that used stderr for prompts).
- David


More information about the SMT-LIB mailing list