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

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
SPASS-SATTPar4Par4 Par4 Yices 2.6.2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
SPASS-SATT 0 527 83027.548 83035.5525272882391919 0
2018-CVC4n 0 521 137443.771 137862.0085212822392525 0
Par4 0 518 148916.734 87927.95182862322828 0
Yices 2.6.2 0 515 121723.739 121709.1815152802353131 0
CVC4 0 515 142952.628 143325.725152782373131 0
CVC4-SymBreakn 0 505 202131.903 202582.2435052732324141 0
veriT 0 495 187558.616 187547.3114952632325151 0
SMTInterpol 0 486 250082.398 244020.7494862702166060 0
Z3n 0 447 317735.319 317772.044472282199999 0
OpenSMT2 0 428 368259.173 368251.522428207221118118 0
Ctrl-Ergo 0 407 425587.591 356834.914407240167139139 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 535 176281.834 64378.6025352952401111 0
SPASS-SATT 0 527 83031.018 83034.9625272882391919 0
2018-CVC4n 0 521 137539.041 137860.8085212822392525 0
Yices 2.6.2 0 515 121728.359 121708.2415152802353131 0
CVC4 0 515 143132.718 143324.465152782373131 0
CVC4-SymBreakn 0 505 202223.173 202580.0735052732324141 0
veriT 0 495 187567.496 187545.4314952632325151 0
SMTInterpol 0 486 250082.398 244020.7494862702166060 0
Z3n 0 447 317760.969 317767.144472282199999 0
Ctrl-Ergo 0 444 542492.471 319839.014444255189102102 0
OpenSMT2 0 428 368277.243 368247.382428207221118118 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 295 84047.698 26681.626295295025111 0
SPASS-SATT 0 288 39922.188 39924.218288288025819 0
2018-CVC4n 0 282 86123.945 86342.626282282026425 0
Yices 2.6.2 0 280 59070.985 59048.791280280026631 0
CVC4 0 278 90831.176 90982.437278278026831 0
CVC4-SymBreakn 0 273 111881.322 112123.711273273027341 0
SMTInterpol 0 270 108749.031 105455.906270270027660 0
veriT 0 263 121596.384 121598.964263263028351 0
Ctrl-Ergo 0 255 232707.197 135859.1842552550291102 0
Z3n 0 228 211038.291 211040.782228228031899 0
OpenSMT2 0 207 267235.482 267202.5142072070339118 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 240 87434.136 32896.976240024030611 0
SPASS-SATT 0 239 38308.83 38310.744239023930719 0
2018-CVC4n 0 239 46615.097 46718.182239023930725 0
CVC4 0 237 47501.542 47542.023237023730931 0
Yices 2.6.2 0 235 57857.374 57859.45235023531131 0
veriT 0 232 61171.112 61146.467232023231451 0
CVC4-SymBreakn 0 232 85541.851 85656.362232023231441 0
OpenSMT2 0 221 96241.761 96244.8682210221325118 0
Z3n 0 219 101922.678 101926.357219021932799 0
SMTInterpol 0 216 136533.367 133764.843216021633060 0
Ctrl-Ergo 0 189 304985.274 179179.831890189357102 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 392 4793.327 4769.744392229163154154 0
Par4 0 385 9154.446 5236.39385216169161161 0
SPASS-SATT 0 381 5217.609 5217.77381219162165165 0
CVC4 0 332 6179.676 6177.607332182150214214 0
veriT 0 328 6244.773 6244.765328174154218218 0
2018-CVC4n 0 314 6471.205 6467.019314170144232232 0
Z3n 0 283 6937.837 6933.156283146137263263 0
OpenSMT2 0 278 7230.787 7224.558278144134268268 0
SMTInterpol 0 276 9050.096 7576.249276167109270270 0
Ctrl-Ergo 0 267 10902.263 7788.718267149118279279 0
CVC4-SymBreakn 0 261 8175.341 8167.78261147114285285 0

n Non-competing.