[SMT-COMP] Results of test jobs for the Single Query track

Giles Reger giles.reger at manchester.ac.uk
Thu May 30 03:24:39 EDT 2019


Dear SMT-COMP participants,

We have now run a small test job on StarExec to exercise all Single Query track solvers on a small number of benchmarks from each division.

This job is available here

https://www.starexec.org/starexec/secure/details/job.jsp?id=34898

Note that this job uses the competition post-processor, which is quite lenient and some errors will appear as ‘unknown’ e.g. the post-processor did not find a result in the output.

An extra job running with a strict post-processor has started running here

https://www.starexec.org/starexec/secure/details/job.jsp?id=34910

and should finish soon. This should pick up the above missed errors but also produces some ‘false positives’ e.g. where a status is printed multiple times.

Note that it is advisable that you copy the testing space to your personal space and run a test job yourself once you have made any fixes. When doing so you should use the 2019 non-incremental scrambler as preprocessor and similarly for the post processor.

As with other tracks, it is also important that you check that your solver has been tested in the correct divisions as these are the divisions that will be used in the competition.

Cheers,
Giles



More information about the SMT-COMP mailing list