Evaluating the 2015 SMT competition

This thesis is an evaluation of the 2015 SMT Competition (SMT-COMP), acompetition for Satisfiability Modulo Theories solvers. SMT-COMP has, since itsinception in 2005, been key for standardising and evaluating the state of SMT. Thethesis attempts to give a complementary view to the results of the competition withalternative measurements and viewpoints by examining the raw results of thecompetition. One of main focuses of the thesis was the impact of the benchmarks used in thecompetition. It is concluded that the majority of the benchmarks in the competitionare trivial. In under a second, some solver solved 95.7 % of the benchmarks andall solvers solved 67.2% of the benchmarks. These easy benchmarks impactsthe main results of the competition. Another noteworthy conclusion is that there isa statistically significant difference between the difficulty of solving the satisfiableand unsatisfiable benchmarks in the competition, with unsatisfiable being easier in general. The other main focus of the thesis was the performance of the solvers, where theconclusion is that that most participating solvers were better than all others onsome benchmarks, either speed-wise or by being the only one solving it. Two solvers stand out in particular, Yices2 for its excellency in speed and Z3 for itsbreadth. The thesis also concludes that for SMT-COMP 2015, parallelism has little to none impact on the results