SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_ABV (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BoolectorPar4Poolector Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Boolector 0 7520 63909.807 63883.2847520516023601818 0
Par4 0 7518 66599.68 54472.467518515923592020 0
2018-Boolectorn 0 7515 76014.897 75990.6547515515523602323 0
Yices 2.6.2 0 7512 93508.913 93548.8477512515823542626 0
Poolector 0 7512 99131.528 72714.1337512515923532626 0
CVC4 0 7458 205434.874 207621.3437458513623228080 0
Z3n 0 7455 229875.125 229878.6897455513023258383 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 7520 68137.25 51792.2617520515923611818 0
Poolector 0 7520 111313.528 61433.347520516023601818 0
Boolector 0 7520 63913.337 63882.4447520516023601818 0
2018-Boolectorn 0 7515 76019.587 75989.7747515515523602323 0
Yices 2.6.2 0 7512 93513.613 93547.6977512515823542626 0
CVC4 0 7458 207477.384 207617.3837458513623228080 0
Z3n 0 7455 229893.035 229875.1997455513023258383 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 5160 15716.984 4678.765516051600237818 0
Boolector 0 5160 10128.291 10098.744516051600237818 0
Par4 0 5159 9951.011 5110.068515951590237918 0
Yices 2.6.2 0 5158 16487.626 16508.882515851580238026 0
2018-Boolectorn 0 5155 20655.984 20628.543515551550238323 0
CVC4 0 5136 66042.951 66180.52513651360240280 0
Z3n 0 5130 81866.505 81860.238513051300240883 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2361 58186.24 46682.193236102361517718 0
Boolector 0 2360 53785.046 53783.7236002360517818 0
2018-Boolectorn 0 2360 55363.603 55361.231236002360517823 0
Poolector 0 2360 95596.545 56754.575236002360517818 0
Yices 2.6.2 0 2354 77025.988 77038.815235402354518426 0
Z3n 0 2325 148026.53 148014.961232502325521383 0
CVC4 0 2322 141434.432 141436.862232202322521680 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 7476 3757.63 2444.5257476514023366262 0
Poolector 0 7460 7054.415 4218.697460513723237878 0
Boolector 0 7440 3736.126 3701.7367440511723239898 0
Yices 2.6.2 0 7427 4123.537 4154.32742751172310111111 0
2018-Boolectorn 0 7425 4872.715 4871.149742551082317113113 0
CVC4 0 7392 6209.573 6191.473739250982294146146 0
Z3n 0 7344 6575.188 6553.871734450642280194194 0

n Non-competing.