[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