SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

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 2019-07-23 17:56:09 +0000

Benchmarks: 2841
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 2597 677556.997 616433.775259712121385244187 57
Yices 2.6.2 0 2164 1681986.24 1682107.466216410651099677677 0
Z3n 0 2081 1834876.671 1835365.162208110661015760602 156
2018-Z3n 0 2075 1850123.97 1850733.561207510631012766608 156
SMTRAT-MCSAT 0 1973 2144115.154 2144263.15619739631010868864 4
veriT+raSAT+Redlog 0 1869 2354843.112 2354276.76918698541015972972 0
CVC4 0 1778 2751336.709 2769255.4631778537124110631063 0
CVC4-SymBreakn 0 1708 2820827.97 2827304.7251708475123311331133 0
MathSAT-default 0 1698 2800090.263 2800342.7651698491120711431142 1
SMT-RAT 0 1696 2793536.872 2793759.463169683885811451129 10
MathSAT-na-ext 0 1653 2910508.221 2910679.7871653448120511881188 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2613 705823.387 600324.226261312241389228171 57
Yices 2.6.2 0 2164 1682098.73 1682083.516216410651099677677 0
Z3n 0 2081 1835040.241 1835339.402208110661015760602 156
2018-Z3n 0 2075 1850291.31 1850706.701207510631012766608 156
SMTRAT-MCSAT 0 1973 2144232.594 2144232.44619739631010868864 4
veriT+raSAT+Redlog 0 1870 2355012.932 2354111.07918708551015971971 0
CVC4 0 1778 2768511.569 2769210.0031778537124110631063 0
CVC4-SymBreakn 0 1708 2826404.78 2827259.5551708475123311331133 0
MathSAT-default 0 1698 2800292.283 2800297.6751698491120711431142 1
SMT-RAT 0 1696 2793766.172 2793715.853169683885811451129 10
MathSAT-na-ext 0 1653 2910730.171 2910633.8671653448120511881188 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1224 316878.4 248173.1961224122401617171 57
Z3n 0 1066 601549.548 601536.0651066106601775602 156
Yices 2.6.2 0 1065 620317.022 620319.5381065106501776677 0
2018-Z3n 0 1063 609783.414 609784.9961063106301778608 156
SMTRAT-MCSAT 0 963 852331.327 852332.22596396301878864 4
veriT+raSAT+Redlog 0 855 1113565.504 1113004.53485585501986971 0
SMT-RAT 0 838 1147028.617 1147039.248838838020031129 10
CVC4 0 537 2022571.417 2023229.008537537023041063 0
MathSAT-default 0 491 1990114.267 1990116.461491491023501142 1
CVC4-SymBreakn 0 475 2062791.973 2063257.826475475023661133 0
MathSAT-na-ext 0 448 2096615.506 2096619.695448448023931188 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1389 93744.986 56951.031389013891452171 57
CVC4 0 1241 450740.151 450780.99512410124116001063 0
CVC4-SymBreakn 0 1233 468412.807 468801.72912330123316081133 0
MathSAT-default 0 1207 514978.016 514981.21412070120716341142 1
MathSAT-na-ext 0 1205 518914.666 518814.17212050120516361188 0
Yices 2.6.2 0 1099 766581.708 766563.9771099010991742677 0
Z3n 0 1015 940116.622 940101.8641015010151826602 156
veriT+raSAT+Redlog 0 1015 946247.428 945906.5451015010151826971 0
2018-Z3n 0 1012 947135.857 947136.5591012010121829608 156
SMTRAT-MCSAT 0 1010 996701.267 996700.221010010101831864 4
SMT-RAT 0 858 1351537.555 1351476.604858085819831129 10

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2416 17677.202 12815.527241611311285425368 57
Z3n 0 2049 21794.571 21764.854204910391010792636 156
2018-Z3n 0 2042 21885.66 21885.941204210351007799643 156
Yices 2.6.2 0 2005 21082.834 21063.65620051013992836836 0
veriT+raSAT+Redlog 0 1817 25536.69 25520.968181782898910241024 0
SMTRAT-MCSAT 0 1816 26773.837 26767.603181694687010251021 4
SMT-RAT 0 1527 33215.088 33211.721152781771013141304 10
MathSAT-default 0 1507 35199.962 35198.1231507426108113341333 1
MathSAT-na-ext 0 1461 36402.042 36362.1131461390107113801380 0
CVC4 0 1340 39160.557 39126.3811340280106015011501 0
CVC4-SymBreakn 0 1299 40075.742 40080.832129932397615421542 0

n Non-competing.