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

BV (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 770 145888.247 132036.2287702215495353 0
Q3B 0 736 210609.263 203206.7957362225148777 5
2018-CVC4n 0 722 288362.963 292450.698722191531101101 0
CVC4 0 722 329819.695 335480.056722189533101101 0
Poolector 0 702 315355.176 296839.783702219483121121 0
Boolector 0 691 338246.91 328328.358691210481132132 0
Z3n 0 688 331791.805 331816.012688198490135134 0
UltimateEliminator+MathSAT-5.5.4 0 274 364065.202 362363.8562749265549138 10

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 777162126.297123607.517772265514646 0
Q3B 0 741218253.473198536.8057412255168272 5
2018-CVC4n 0 722291188.913292445.478722191531101101 0
CVC4 0 722333430.045335475.076722189533101101 0
Poolector 0 711343502.886287805.665711223488112112 0
Boolector 0 698344389.78323873.368698214484125125 0
Z3n 0 688331830.275331810.002688198490135134 0
UltimateEliminator+MathSAT-5.5.4 0 274392041.302361021.5062749265549132 10

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 22662329.28437328.871226226059746 0
Q3B 0 22544707.62134362.751225225059872 5
Poolector 0 22371316.05544962.4882232230600112 0
Boolector 0 21474742.67366401.9512142140609125 0
Z3n 0 19896217.29796217.6041981980625134 0
2018-CVC4n 0 191154577.722155633.6991911910632101 0
CVC4 0 189201052.813202877.3631891890634101 0
UltimateEliminator+MathSAT-5.5.4 0 9234551.169213346.58990814132 10

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 55142197.01328678.639551055127246 0
CVC4 0 53374777.23274997.7135330533290101 0
2018-CVC4n 0 53179011.1979211.7795310531292101 0
Q3B 0 516115945.853106574.054516051630772 5
Z3n 0 490178012.978177992.3984900490333134 0
Poolector 0 488214586.831185243.1774880488335112 0
Boolector 0 484212047.107199871.4174840484339125 0
UltimateEliminator+MathSAT-5.5.4 0 265112383.498106851.5392650265558132 10

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 7423643.6472428.247422085348181 0
Q3B 0 7134031.0693121.869713205508110100 5
Poolector 0 6646433.6464600.048664208456159159 0
Z3n 0 6554475.364453.575655192463168168 0
Boolector 0 6435108.2674771.941643196447180180 0
CVC4 0 6265357.7245355.033626108518197197 0
2018-CVC4n 0 6076058.3056056.13360797510216216 0
UltimateEliminator+MathSAT-5.5.4 0 2726301.4735504.5432728264551150 10

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.