SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2016

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_ABV (Main Track)

Competition results for the QF_ABV division as of Thu Jul 7 07:24:34 GMT

Benchmarks in this division : 14720

Winners

Sequential Performance Parallel Performance
Boolector Boolector

Result table1

Sequential Performance

Solver Error Score Correct Score avg. CPU time
Boolector 0.000 14401.055 78.180
CVC4 0.000 13280.280 256.177
MathSat5n 0.000 13437.758 256.599
Yices2 0.000 14334.777 93.958
z3n 0.000 13207.834 288.569

Parallel Performance

SolverError Score Correct Score avg. CPU time avg. WALL time Unsolved
Boolector 0.000 14401.055 78.210 78.129 34
CVC4 0.000 13280.280 256.195 260.609 105
MathSat5n 0.000 13450.473 256.698 256.543 90
Yices2 0.000 14334.777 93.991 93.906 45
z3n 0.000 13207.834 288.698 288.544 244

n. Non-competitive.

1. Scores are computed according to Section 7 of the rules.