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_AUFBV (Single Query Track)

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

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

Benchmarks: 41
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 38 7610.364 7611.7283873133 0
Z3n 0 38 9823.537 9820.2233863233 0
Boolector 0 32 16.484 16.4933262690 0
Poolector 0 32 46.707 18.0853262690 0
2018-CVC4n 0 32 22957.184 23088.1893262699 0
CVC4 0 32 23514.085 23657.383262699 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 38 7611.514 7611.5683873133 0
Z3n 0 38 9824.307 9820.1233863233 0
Boolector 0 32 16.484 16.4933262690 0
Poolector 0 32 46.707 18.0853262690 0
2018-CVC4n 0 32 23079.294 23087.7593262699 0
CVC4 0 32 23647.855 23656.933262699 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 7 235.901 235.935770343 0
Boolector 0 6 0.154 0.159660350 0
Poolector 0 6 1.231 1.235660350 0
Z3n 0 6 2400.441 2400.441660353 0
2018-CVC4n 0 6 2400.568 2400.566660359 0
CVC4 0 6 2400.585 2400.583660359 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 32 7423.866 7419.6823203293 0
Yices 2.6.2 0 31 7375.613 7375.63331031103 0
Boolector 0 26 16.33 16.33426026150 0
Poolector 0 26 45.476 16.8526026150 0
2018-CVC4n 0 26 20678.725 20687.19226026159 0
CVC4 0 26 21247.27 21256.34726026159 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 35 167.933 167.943562966 0
Boolector 0 32 16.484 16.4933262690 0
Poolector 0 32 46.707 18.0853262690 0
CVC4 0 31 257.645 257.64316251010 0
2018-CVC4n 0 31 257.694 257.689316251010 0
Z3n 0 31 264.868 260.109316251010 0

n Non-competing.