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

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
OpenSMTOpenSMTOpenSMT OpenSMT Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
OpenSMT 0 406 44406.525 44349.8084062141922323 0
2019-SPASS-SATTn 0 405 49274.878 49247.124052151902424 0
2019-Par4n 0 396 78462.172 49467.3183962161803333 0
CVC4 0 391 83335.57 83578.6293912041873838 0
Yices2 0 389 66776.562 66727.963892091804040 0
Yices2-fixedn 0 389 66849.747 66839.663892091804040 0
z3n 0 385 78656.762 78634.6853852051804444 0
veriT 0 377 91357.696 91356.5633771971805252 0
SMTInterpol-fixedn 0 358 137373.773 132691.9813582021567171 0
SMTInterpol 0 354 137016.606 132499.3173541991557575 0
MathSAT5n 0 353 121704.137 121721.3813531961577676 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 412 101647.572 40989.8884122181941717 0
OpenSMT 0 406 44408.805 44349.4184062141922323 0
2019-SPASS-SATTn 0 405 49277.548 49246.064052151902424 0
CVC4 0 391 83469.31 83576.7693912041873838 0
Yices2 0 389 66778.422 66726.633892091804040 0
Yices2-fixedn 0 389 66852.017 66838.33892091804040 0
z3n 0 385 78661.172 78633.5353852051804444 0
veriT 0 377 91363.646 91354.8033771971805252 0
SMTInterpol-fixedn 0 358 137373.773 132691.9813582021567171 0
SMTInterpol 0 357 137030.506 132435.0073572011567272 0
MathSAT5n 0 353 121713.847 121718.8113531961577676 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 218 31105.66 13272.57218218021117 0
2019-SPASS-SATTn 0 215 17727.838 17717.084215215021424 0
OpenSMT 0 214 20594.628 20588.407214214021523 0
Yices2-fixedn 0 209 24065.572 24060.634209209022040 0
Yices2 0 209 24131.695 24079.949209209022040 0
z3n 0 205 31111.677 31113.216205205022444 0
CVC4 0 204 44407.138 44506.088204204022538 0
SMTInterpol-fixedn 0 202 50320.975 47621.971202202022771 0
SMTInterpol 0 201 49935.475 47269.123201201022872 0
veriT 0 197 46453.619 46442.852197197023252 0
MathSAT5n 0 196 49066.078 49068.665196196023376 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 194 65741.912 22917.318194019423517 0
OpenSMT 0 192 19014.177 18961.011192019223723 0
2019-SPASS-SATTn 0 190 26749.71 26728.976190019023924 0
CVC4 0 187 34262.172 34270.681187018724238 0
Yices2 0 180 37846.727 37846.681180018024940 0
Yices2-fixedn 0 180 37986.445 37977.666180018024940 0
veriT 0 180 40110.027 40111.95180018024952 0
z3n 0 180 42749.496 42720.319180018024944 0
MathSAT5n 0 157 67847.769 67850.146157015727276 0
SMTInterpol-fixedn 0 156 82252.798 80270.01156015627371 0
SMTInterpol 0 156 82295.031 80365.884156015627372 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 312 3717.279 3701.814312181131117117 0
Yices2 0 311 3705.552 3701.613311180131118118 0
2019-SPASS-SATTn 0 306 4150.167 4116.67306171135123123 0
OpenSMT 0 305 4144.049 4112.369305155150124124 0
2019-Par4n 0 294 7490.423 4341.293294162132135135 0
z3n 0 259 4951.217 4920.281259146113170170 0
CVC4 0 258 5068.721 5061.763258142116171171 0
veriT 0 256 4934.931 4922.593256133123173173 0
MathSAT5n 0 245 4985.407 4985.539245141104184184 0
SMTInterpol-fixedn 0 212 7316.731 6082.11621212983217217 0
SMTInterpol 0 212 7311.95 6084.70221213082217217 0

n Non-competing.