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_UFBV (Main Track)

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

Benchmarks in this division: 31
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 31.000 50.299 0
CVC4 0.000 25.948 473.051 6
Yices2 0.000 26.790 328.764 5
mathsat-5.4.1n 0.000 20.896 541.958 12
z3-4.5.0n 0.000 16.686 652.168 17

Parallel Performance

Solver Error Score Correct Score CPU Score WALL Score Unsolved
Boolector 0.000 31.000 50.299 52.143 0
CVC4 0.000 25.948 473.052 473.127 6
Yices2 0.000 26.790 328.764 328.792 5
mathsat-5.4.1n 0.000 20.896 541.958 542.022 12
z3-4.5.0n 0.000 16.686 652.169 652.902 17

n. Non-competing.

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