SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_NRA (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 2230
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 Yices2 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1998 325585.346 294271.29819989371061232180 52
Yices2-fixedn 0 1770 579351.637 580091.8661770816954460460 0
Yices2 0 1770 580322.491 580314.7971770816954460460 0
z3n 0 1658 708539.767 708566.3951658830828572566 0
SMT-RAT-MCSAT 0 1564 808770.651 808779.0781564751813666632 8
veriT+raSAT+Redlog 0 1420 975715.937 975662.6841420635785810808 0
SMT-RAT-CAlC 0 1377 1045700.847 1045791.5581377652725853845 7
CVC4 0 1325 1169585.429 1179419.7851325385940905905 0
MathSAT5n 0 1292 1155961.421 1156078.1821292361931938938 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2010 333813.256 287439.95820109461064220168 52
Yices2-fixedn 0 1770 580033.882 580073.8961770816954460460 0
Yices2 0 1770 580374.371 580298.6471770816954460460 0
z3n 0 1658 708610.427 708547.1951658830828572566 0
SMT-RAT-MCSAT 0 1564 808820.671 808759.1981564751813666632 8
veriT+raSAT+Redlog 0 1420 975761.947 975644.6941420635785810808 0
SMT-RAT-CAlC 0 1377 1045783.947 1045762.0181377652725853845 7
CVC4 0 1326 1179005.929 1179094.7761326385941904904 0
MathSAT5n 0 1292 1156089.651 1156039.5821292361931938938 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 946 134294.83 104843.31594694601284168 52
z3n 0 830 237748.324 237699.53683083001400566 0
Yices2 0 816 254741.897 254706.17681681601414460 0
Yices2-fixedn 0 816 254729.098 254746.90181681601414460 0
SMT-RAT-MCSAT 0 751 316588.126 316577.98675175101479632 8
SMT-RAT-CAlC 0 652 443829.654 443811.59165265201578845 7
veriT+raSAT+Redlog 0 635 465121.218 465053.78863563501595808 0
CVC4 0 385 826466.362 826835.5638538501845904 0
MathSAT5n 0 361 800695.491 800697.57236136101869938 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1064 42318.426 25396.6431064010641166168 52
Yices2-fixedn 0 954 168104.784 168126.99595409541276460 0
Yices2 0 954 168432.474 168392.47195409541276460 0
CVC4 0 941 195339.568 195059.21794109411289904 0
MathSAT5n 0 931 198194.16 198142.0193109311299938 0
z3n 0 828 316040.786 316026.3482808281402566 0
SMT-RAT-MCSAT 0 813 336463.282 336411.55481308131417632 8
veriT+raSAT+Redlog 0 785 354551.18 354501.65278507851445808 0
SMT-RAT-CAlC 0 725 444754.293 444750.42772507251505845 7

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1889 14257.489 10323.97218898891000341289 52
Yices2 0 1666 14357.316 14358.1321666779887564564 0
Yices2-fixedn 0 1666 14363.767 14364.9131666779887564564 0
z3n 0 1593 17711.919 17691.0941593802791637632 0
SMT-RAT-MCSAT 0 1445 20675.031 20652.751445730715785777 8
veriT+raSAT+Redlog 0 1394 20733.113 20721.2031394619775836836 0
SMT-RAT-CAlC 0 1251 25197.195 25171.8471251646605979972 7
MathSAT5n 0 1163 27996.385 27995.378116331784610671067 0
CVC4 0 1002 31768.353 31728.2100219780512281228 0

n Non-competing.