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

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4CVC4 SMTInterpol Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2447 93732.847 80352.6172447137610716161 0
MathSAT5n 0 2329 443942.69 443796.202232913091020179179 0
CVC4 0 2290 318190.742 317946.291229012561034218217 0
z3n 0 2233 519173.25 519200.23622331311922275275 0
Yices2 0 2198 410092.801 410107.013219811811017310310 0
Yices2-fixedn 0 2197 410250.569 410171.974219711801017311311 0
SMTInterpol 0 2170 555671.409 527233.967217010971073338338 0
SMTInterpol-fixedn 0 2168 555846.38 527576.243216810951073340340 0
veriT 0 819 1433613.127 1433714.08381957424516891152 1

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2459 103682.297 74071.7982459138410754949 0
MathSAT5n 0 2329 443971.89 443789.002232913091020179179 0
CVC4 0 2290 318208.962 317939.421229012561034218217 0
z3n 0 2233 519201.44 519189.75622331311922275275 0
Yices2 0 2198 410115.181 410099.193219811811017310310 0
Yices2-fixedn 0 2197 410271.249 410163.744219711801017311311 0
SMTInterpol 0 2170 555671.409 527233.967217010971073338338 0
SMTInterpol-fixedn 0 2170 555863.97 527552.913217010971073338338 0
veriT 0 819 1433703.647 1433672.18381957424516891152 1

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1384 51796.307 31039.904138413840112449 0
z3n 0 1311 215944.195 215929.511311131101197275 0
MathSAT5n 0 1309 200590.763 200464.6021309130901199179 0
CVC4 0 1256 206924.201 206786.281256125601252217 0
Yices2 0 1181 295917.05 295908.8921181118101327310 0
Yices2-fixedn 0 1180 296110.789 296014.2191180118001328311 0
SMTInterpol 0 1097 454690.446 440009.6941097109701411338 0
SMTInterpol-fixedn 0 1097 454844.083 440201.9751097109701411338 0
veriT 0 574 683786.095 683777.036574574019341152 1

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1075 36285.99 27431.894107501075143349 0
SMTInterpol 0 1073 85380.963 71624.2731073010731435338 0
SMTInterpol-fixedn 0 1073 85419.887 71750.9381073010731435338 0
CVC4 0 1034 95684.761 95553.1421034010341474217 0
MathSAT5n 0 1020 227781.127 227724.41020010201488179 0
Yices2-fixedn 0 1017 98560.46 98549.5251017010171491311 0
Yices2 0 1017 98598.131 98590.3011017010171491310 0
z3n 0 922 287657.245 287660.24792209221586275 0
veriT 0 245 734317.552 734295.147245024522631152 1

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2405 7636.104 4497.818240513451060103103 0
Yices2 0 2057 13494.279 13474.497205710571000451451 0
Yices2-fixedn 0 2057 13505.262 13484.435205710571000451451 0
CVC4 0 1797 26411.213 26223.8541797994803711711 0
z3n 0 1524 28434.148 28386.2781524864660984984 0
MathSAT5n 0 1408 29959.777 29920.814140885055811001100 0
SMTInterpol 0 1216 45067.936 37042.005121661560112921292 0
SMTInterpol-fixedn 0 1213 44972.826 37049.903121361260112951295 0
veriT 0 703 33101.615 33066.38870350020318051304 1

n Non-competing.