SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

QF_UFBV (Single Query Track)

Competition results for the QF_UFBV division in the Single Query Track.

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 223
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices 2.6.2Yices 2.6.2Yices 2.6.2 Yices 2.6.2 Yices 2.6.2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 220 19120.64 19122.4422201338733 0
Boolector 0 217 25475.296 25477.1442171338466 0
2018-Boolectorn 0 213 2039.953 2040.27421313281100 0
CVC4 0 213 30579.127 30519.568213132811010 0
Poolector 0 211 43664.445 32580.204211133781212 0
Z3n 0 198 66301.091 66305.626198132662525 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 220 19121.27 19122.3722201338733 0
Poolector 0 218 59220.165 23944.4832181338555 0
Boolector 0 217 25475.496 25476.9742171338466 0
2018-Boolectorn 0 213 2039.953 2040.27421313281100 0
CVC4 0 213 30582.327 30519.228213132811010 0
Z3n 0 198 66305.021 66304.916198132662525 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 133 143.623 143.6321331330903 0
Poolector 0 133 2252.227 589.3541331330905 0
Boolector 0 133 2330.755 2331.2141331330906 0
2018-Boolectorn 0 132 142.195 142.2131321320910 0
Z3n 0 132 2540.217 2539.37513213209125 0
CVC4 0 132 2794.044 2791.49613213209110 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 87 18977.647 18978.739870871363 0
Poolector 0 85 56967.938 23355.13850851385 0
Boolector 0 84 23144.741 23145.76840841396 0
2018-Boolectorn 0 81 1897.758 1898.061810811420 0
CVC4 0 81 27788.282 27727.7318108114210 0
Z3n 0 66 63764.804 63765.5426606615725 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Boolectorn 0 198 696.776 696.869198132662515 0
Yices 2.6.2 0 194 787.632 787.64194132622929 0
Boolector 0 193 1023.545 1023.602193130633030 0
Poolector 0 189 1778.455 1086.55189130593434 0
CVC4 0 188 1384.395 1379.88188132563535 0
Z3n 0 182 1121.123 1120.285182131514141 0

n Non-competing.