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

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 UNSATUnsolvedTimeout 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 Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 777 162126.297 123607.517772265514646 0
Q3B 0 741 218253.473 198536.8057412255168272 5
2018-CVC4n 0 722 291188.913 292445.478722191531101101 0
CVC4 0 722 333430.045 335475.076722189533101101 0
Poolector 0 711 343502.886 287805.665711223488112112 0
Boolector 0 698 344389.78 323873.368698214484125125 0
Z3n 0 688 331830.275 331810.002688198490135134 0
UltimateEliminator+MathSAT-5.5.4 0 274 392041.302 361021.5062749265549132 10

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 226 62329.284 37328.871226226059746 0
Q3B 0 225 44707.621 34362.751225225059872 5
Poolector 0 223 71316.055 44962.4882232230600112 0
Boolector 0 214 74742.673 66401.9512142140609125 0
Z3n 0 198 96217.297 96217.6041981980625134 0
2018-CVC4n 0 191 154577.722 155633.6991911910632101 0
CVC4 0 189 201052.813 202877.3631891890634101 0
UltimateEliminator+MathSAT-5.5.4 0 9 234551.169 213346.58990814132 10

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 551 42197.013 28678.639551055127246 0
CVC4 0 533 74777.232 74997.7135330533290101 0
2018-CVC4n 0 531 79011.19 79211.7795310531292101 0
Q3B 0 516 115945.853 106574.054516051630772 5
Z3n 0 490 178012.978 177992.3984900490333134 0
Poolector 0 488 214586.831 185243.1774880488335112 0
Boolector 0 484 212047.107 199871.4174840484339125 0
UltimateEliminator+MathSAT-5.5.4 0 265 112383.498 106851.5392650265558132 10

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 742 3643.647 2428.247422085348181 0
Q3B 0 713 4031.069 3121.869713205508110100 5
Poolector 0 664 6433.646 4600.048664208456159159 0
Z3n 0 655 4475.36 4453.575655192463168168 0
Boolector 0 643 5108.267 4771.941643196447180180 0
CVC4 0 626 5357.724 5355.033626108518197197 0
2018-CVC4n 0 607 6058.305 6056.13360797510216216 0
UltimateEliminator+MathSAT-5.5.4 0 272 6301.473 5504.5432728264551150 10

n Non-competing.