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

[Vijay Ganesh]

Dear Tjark,

Thanks a ton to you and other organizers!!

Jimmy and Mate,

Can we please respond asap to Tjark's requests.

Cheers,
Vijay Ganesh.
https://ece.uwaterloo.ca/~vganesh

________________________________________
From: smt-comp-bounces at cs.nyu.edu [smt-comp-bounces at cs.nyu.edu] on behalf of Tjark Weber [tjark.weber at it.uu.se]
Sent: Saturday, June 04, 2016 1:42 PM
To: smt-comp at cs.nyu.edu; jliang at gsd.uwaterloo.ca; soos.mate at gmail.com
Cc: David Deharbe; Sylvain Conchon
Subject: [SMT-COMP] SMT-COMP 2016: Application Track Testing

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

_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
http://cs.nyu.edu/mailman/listinfo/smt-comp