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

[Vijay Ganesh]

Thanks again Mate, Jimmy, Trevor, and organizers!

Cheers,
Vijay Ganesh.
https://ece.uwaterloo.ca/~vganesh
________________________________
From: Jimmy Liang [paradoxical.reasoning at gmail.com]
Sent: Monday, June 06, 2016 11:08 PM
To: Mate Soos
Cc: Vijay Ganesh; Tjark Weber; smt-comp at cs.nyu.edu; jliang at gsd.uwaterloo.ca; David Deharbe; Sylvain Conchon
Subject: Re: [SMT-COMP] SMT-COMP 2016: Application Track Testing

Dear Dr. Weber,

I have also updated the solvers.

1. MapleSTP-fixed (id: 8245)
2. MapleSTP-mt-fixed (id: 8246)

They run in the same manner as Mate's STP, that is via starexec_run_default.

Thank you for the heads up, and please let me know if any other issues arise.

Sincerely,
Jia Liang

On Mon, Jun 6, 2016 at 8:32 PM, Mate Soos <soos.mate at gmail.com<mailto:soos.mate at gmail.com>> wrote:
Dear Tjark,

First of all, thanks for letting us know things weren't good and letting
us fix it!

I have submitted the new versions. They all need to be called as per
starexec_run_default, but of course the $1 needs to be empty. It will
then read from the console (the command line options in
starexec_run_default are important, though). I have fixed the issue, I'd
be really glad if you could check it. It seems to work under trace-exec,
though trace-exec doesn't pass the parameters of course. The new names are:

stp-cms-minisat-fixed-2016 [ID: 8243]
stp-cms-st-fixed-2016 [ID: 8242]
stp-cms-mt-fixed-2016 [ID: 8241]
stp-cms-exp-fixed-2016 [ID: 8244]

Please let me know if these pass the muster. I hope they do.


By the way, we have observed a strange crash on StarExec with the
multi-threaded executable (stp-cms-mt-2016) of the main competition. The
corresponding executable works fine on our machines, and in deeper
inspection it seems that StarExec limits the stack size to lower than
what is on our machines or the distributed official StarExec OVA. This
causes our solver to crash.

https://www.starexec.org/starexec/secure/details/pairsInSpace.jsp?type=unknown&sid=560017&configid=158183&stagenum=1

This is not reproducible with the OVA distributed by StarExec, as it's a
runtime setting by the execution environment (hence it took us a week to
track it down). I'm wondering if it would be possible to re-run those 28
SMTLIB2 inputs with a larger stack on StarExec? We perform extensive
testing and never hit this issue, so I'm wondering if we could get an
edge-case exemption and allow us a re-run of those files with a larger
stack ("ulimit -s 8192", standard on Linux, works here, distributed OVA
has "ulimit -s 10240", works too).

Thanks a lot again for all your work and letting us fix up the
interactive solver!

Mate

On 06/04/2016 07:07 PM, Vijay Ganesh wrote:
> 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<mailto:smt-comp-bounces at cs.nyu.edu> [smt-comp-bounces at cs.nyu.edu<mailto:smt-comp-bounces at cs.nyu.edu>] on behalf of Tjark Weber [tjark.weber at it.uu.se<mailto:tjark.weber at it.uu.se>]
> Sent: Saturday, June 04, 2016 1:42 PM
> To: smt-comp at cs.nyu.edu<mailto:smt-comp at cs.nyu.edu>; jliang at gsd.uwaterloo.ca<mailto:jliang at gsd.uwaterloo.ca>; soos.mate at gmail.com<mailto: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<mailto:SMT-COMP at cs.nyu.edu>
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>