[SMT-COMP] SMT-COMP 2016: Application Track Testing

[Tjark Weber]

Jimmy, Mate,

During preliminary testing for the application track, we noticed issues
with the MapleSTP* and STP-* solvers. These solvers get stuck when run
by the trace executor, resulting in a score of 0 correct answers on
each benchmark.

MapleSTP* does not seem to respond with "success" to the initial
"(set-option :print-success true)" command, as mandated by Section
4.2.1 of the SMT-LIB standard.

For STP-*, the issue seems to be more complicated: an fgetc call in the
trace executor blocks. Perhaps the solver's output stream needs to be
flushed?

To obtain more meaningful application track results, we will accept
updated versions of your solvers that work with the trace executor
until *** June 7 ***. Please submit new versions as usual, by uploading
them to StarExec (in a space that is visible to us) and emailing us the
new solver IDs.

Note that the trace executor sources are available from
http://smtcomp.sourceforge.net/2016/tools.shtml
in case you want to run your own tests.

Best,
Tjark