[SMT-COMP] problems with Colibri StarExec configuration script

Aina Niemetz aina.niemetz at gmail.com
Sat Jun 29 09:25:21 EDT 2019


Francois,

we're having problems with the StarExec configuration script you
provided for Colibri. For the Single Query Track, we had to wrap all
solvers because the 'runsolver' script, which runs the job on the
cluster node, combines stderr and stdout (which is against the rules
since we should only consider what the solver outputs on stdout).

As a consequence, we had to rename the original starexec_run_default to
'original_starexec_run_default' and provide a starexec_run_default file
that wraps the original one in a way that the stderr output is preserved
in an additional output file.

Colibri, however, checks for the name of the configuration file, and if
it does not start with 'starexec_run_' it aborts with 'BAD COMMAND
NAME'. This obviously resulted in Colibri aborting on all benchmarks.

I will fix this and rerun Colibri. It will still run competitively.

This is mainly FYI for you and everybody to know what's happening.
And also, don't do this. It breaks our setup.

Thanks,
Aina

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190629/79c20cb4/attachment.asc>


More information about the SMT-COMP mailing list