SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2017

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_ABV (Main Track)

Competition results for the QF_ABV division as of Fri Jul 21 10:18:02 GMT

Benchmarks in this division : 15061
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
Boolector Boolector

Result table1

Sequential Performance

Solver Error Score Correct Score CPU Time Unsolved
Boolector 0.000 14627.624 56.054 40
CVC4 0.000 13136.950 155.681 139
Yices2 0.000 14515.846 65.395 56
mathsat-5.4.1n 0.000 13098.157 155.650 122
z3-4.5.0n 0.000 13115.900 171.596 172

Parallel Performance

Solver Error Score Correct Score CPU Score WALL Score Unsolved
Boolector 0.000 14627.624 56.054 56.101 40
CVC4 0.000 13136.950 155.681 162.762 139
Yices2 0.000 14515.846 65.395 65.207 56
mathsat-5.4.1n 0.000 13098.157 155.651 155.727 122
z3-4.5.0n 0.000 13115.900 171.597 171.665 172

n. Non-competing.

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