[SMT-COMP] SMT-EVAL 2013 data release

Aaron Stump aaron-stump at uiowa.edu
Fri Dec 20 17:44:59 EST 2013


Dear colleagues interested in SMT-COMP and SMT-EVAL,

We are happy to announce that the SMT-EVAL 2013 workload, which consists of
running 45 solvers (current and historic) on all of the benchmarks in the
current version (last updated Summer 2012) of the SMT-LIB, has completed
now on StarExec. We ran the 1663478 job pairs for this workload (a job pair
is a single benchmark being run by a single solver) in four groups of
roughly a quarter the total size each. We are making the raw data public
now, for your feedback and interest. We will also be working to analyze and
summarize the data in the new year, along with other aspects of our
evaluation. You can find the jobs on the StarExec web site here, via the
"guest" access link at the bottom left of the page:

https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=4566

Using the navigator on the left side of the page, navigate to
root/SMT/Competitions and evaluations/SMT-EVAL 2013/To Run. The data from
the evaluation is in the subspaces with names that look like

Run every 4-th benchmark - group X

Select one of the groups and then expand the "jobs" collapsible table on
the right part of the screen, and click on the name of the displayed job.
You will then get a job explorer page, where you can see summary
statistics, navigate into specific subspaces of the job, download job
output (all output from the actual solvers) and job information (a .csv
file with running time info), and use some visualization tools.

Please let us know if you see any unexpected results in the data, and let
Aaron know if you have feedback or encounter bugs with StarExec.

Best wishes,
Aaron, David, and Tjark


More information about the SMT-COMP mailing list