Unwanted output in tests (and probably outside of it, too)

[PhilippWendler]

When running tests, such as in this case, some of the tests seem to print warnings like the following:

• Unexpected logic for quantifier elimination ALL
• WARNING: optimization with quantified constraints is not supported

I am not sure how to interpret this, does this indicate a bug?

Anyway, given that these strings do not appear in the source of JavaSMT, I assume that this outputs will also appear in certain situations during regular usage of JavaSMT (outside of tests). However, JavaSMT and the solvers are libraries, they should never write to stdout or stderr unless explicitly told so by the calling application. Any output is likely to mess up the desired output of the application. Libraries should use logging, or, if the message indicate bugs, communicate this via exceptions.

[kfriedberger]

I fully agree with you. Libraries should not print directly to stdout/stderr.
There have been cases in the past, where we informed the developers and they changed their solver code accordingly.
Someone could collect the solvers with messages and report them.

[kfriedberger]

Related issue: uuverifiers/ostrich#95