SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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 UNSATUnsolvedAbstainedTimeout 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 ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices 2.6.2 0 387611.5147611.5683873133 0
Z3n 0 389824.3079820.1233863233 0
Boolector 0 3216.48416.4933262690 0
Poolector 0 3246.70718.0853262690 0
2018-CVC4n 0 3223079.29423087.7593262699 0
CVC4 0 3223647.85523656.933262699 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 7235.901235.935770343 0
Boolector 0 60.1540.159660350 0
Poolector 0 61.2311.235660350 0
Z3n 0 62400.4412400.441660353 0
2018-CVC4n 0 62400.5682400.566660359 0
CVC4 0 62400.5852400.583660359 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 327423.8667419.6823203293 0
Yices 2.6.2 0 317375.6137375.63331031103 0
Boolector 0 2616.3316.33426026150 0
Poolector 0 2645.47616.8526026150 0
2018-CVC4n 0 2620678.72520687.19226026159 0
CVC4 0 2621247.2721256.34726026159 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices 2.6.2 0 35167.933167.943562966 0
Boolector 0 3216.48416.4933262690 0
Poolector 0 3246.70718.0853262690 0
CVC4 0 31257.645257.64316251010 0
2018-CVC4n 0 31257.694257.689316251010 0
Z3n 0 31264.868260.109316251010 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.