[SMT-COMP] StarExec questions

Delcypher delcypher at gmail.com
Mon Jun 12 10:36:53 EDT 2017


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

More information about the SMT-COMP mailing list