[SMT-COMP] StarExec questions

[Giles Reger]

Hi,

No preprocessor should be required to check the output of your tool.

In `SMT-COMP 2016 (273)’ the 273 is just the identifier of the post processor (e.g. it is the 273rd one that was uploaded). This is the post processor that you should use.

You are correct that the table summarises the results as given by the post processor. However, I don’t always find the numbers in this table that helpful and tend to rely more on the downloaded CSV file (see next). For some post processors “wrong” does not always mean an error.

In the “actions" tab you can download the results of the post processing as a CSV file by selecting “job information”. Hopefully the fields are self-explanatory.

The “job pairs” tab can be used to find the results of particular jobs. You can click on the status of a job to get more information about the job, including the output from the run. This can help debug what is going on. You can also download all unprocessed outputs form the aforementioned “actions” tab.

Hope that helps,
Giles

> On 12 Jun 2017, at 15:36, Delcypher <delcypher at gmail.com> wrote:
> 
> Hi,
> 
> Thanks for the advice.
> 
> I managed to get most things working in the end by building my tool in
> a Docker container. One thing that is unclear to me is how the results
> of a run can be processed.
> 
> What I'd like to do is run my solver over the some of the available
> SMT-LIB benchmarks that are annotated with their expected
> satisfiability and have StarExec check the result.
> Presumably I need to run a particular pre and post processor for this.
> 
> * What pre and post processor should I run? It unclear which one I should use.
> E.g. `SMT-COMP 2016 (273)`. What does the `273` number mean?
> 
> * Where are the results of the post-processor shown and how can they
> be downloaded? E.g. When I run a job [1]
> I see a table that says "solver summary" that I presume is the result
> of running the `SMT-COMP 2016 (273)`
> post-processor.  Is that right?
> 
> 
> [1] https://www.starexec.org/starexec/secure/details/job.jsp?anonId=7df0b214-09a4-42cb-8692-8a606ae05105
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp