The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
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
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| OpenSMT | OpenSMT | OpenSMT | OpenSMT | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 406 | 44406.525 | 44349.808 | 406 | 214 | 192 | 23 | 23 | 0 | |
| 2019-SPASS-SATTn | 0 | 405 | 49274.878 | 49247.12 | 405 | 215 | 190 | 24 | 24 | 0 | |
| 2019-Par4n | 0 | 396 | 78462.172 | 49467.318 | 396 | 216 | 180 | 33 | 33 | 0 | |
| CVC4 | 0 | 391 | 83335.57 | 83578.629 | 391 | 204 | 187 | 38 | 38 | 0 | |
| Yices2 | 0 | 389 | 66776.562 | 66727.96 | 389 | 209 | 180 | 40 | 40 | 0 | |
| Yices2-fixedn | 0 | 389 | 66849.747 | 66839.66 | 389 | 209 | 180 | 40 | 40 | 0 | |
| z3n | 0 | 385 | 78656.762 | 78634.685 | 385 | 205 | 180 | 44 | 44 | 0 | |
| veriT | 0 | 377 | 91357.696 | 91356.563 | 377 | 197 | 180 | 52 | 52 | 0 | |
| SMTInterpol-fixedn | 0 | 358 | 137373.773 | 132691.981 | 358 | 202 | 156 | 71 | 71 | 0 | |
| SMTInterpol | 0 | 354 | 137016.606 | 132499.317 | 354 | 199 | 155 | 75 | 75 | 0 | |
| MathSAT5n | 0 | 353 | 121704.137 | 121721.381 | 353 | 196 | 157 | 76 | 76 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 412 | 101647.572 | 40989.888 | 412 | 218 | 194 | 17 | 17 | 0 | |
| OpenSMT | 0 | 406 | 44408.805 | 44349.418 | 406 | 214 | 192 | 23 | 23 | 0 | |
| 2019-SPASS-SATTn | 0 | 405 | 49277.548 | 49246.06 | 405 | 215 | 190 | 24 | 24 | 0 | |
| CVC4 | 0 | 391 | 83469.31 | 83576.769 | 391 | 204 | 187 | 38 | 38 | 0 | |
| Yices2 | 0 | 389 | 66778.422 | 66726.63 | 389 | 209 | 180 | 40 | 40 | 0 | |
| Yices2-fixedn | 0 | 389 | 66852.017 | 66838.3 | 389 | 209 | 180 | 40 | 40 | 0 | |
| z3n | 0 | 385 | 78661.172 | 78633.535 | 385 | 205 | 180 | 44 | 44 | 0 | |
| veriT | 0 | 377 | 91363.646 | 91354.803 | 377 | 197 | 180 | 52 | 52 | 0 | |
| SMTInterpol-fixedn | 0 | 358 | 137373.773 | 132691.981 | 358 | 202 | 156 | 71 | 71 | 0 | |
| SMTInterpol | 0 | 357 | 137030.506 | 132435.007 | 357 | 201 | 156 | 72 | 72 | 0 | |
| MathSAT5n | 0 | 353 | 121713.847 | 121718.811 | 353 | 196 | 157 | 76 | 76 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 218 | 31105.66 | 13272.57 | 218 | 218 | 0 | 211 | 17 | 0 |
| 2019-SPASS-SATTn | 0 | 215 | 17727.838 | 17717.084 | 215 | 215 | 0 | 214 | 24 | 0 |
| OpenSMT | 0 | 214 | 20594.628 | 20588.407 | 214 | 214 | 0 | 215 | 23 | 0 |
| Yices2-fixedn | 0 | 209 | 24065.572 | 24060.634 | 209 | 209 | 0 | 220 | 40 | 0 |
| Yices2 | 0 | 209 | 24131.695 | 24079.949 | 209 | 209 | 0 | 220 | 40 | 0 |
| z3n | 0 | 205 | 31111.677 | 31113.216 | 205 | 205 | 0 | 224 | 44 | 0 |
| CVC4 | 0 | 204 | 44407.138 | 44506.088 | 204 | 204 | 0 | 225 | 38 | 0 |
| SMTInterpol-fixedn | 0 | 202 | 50320.975 | 47621.971 | 202 | 202 | 0 | 227 | 71 | 0 |
| SMTInterpol | 0 | 201 | 49935.475 | 47269.123 | 201 | 201 | 0 | 228 | 72 | 0 |
| veriT | 0 | 197 | 46453.619 | 46442.852 | 197 | 197 | 0 | 232 | 52 | 0 |
| MathSAT5n | 0 | 196 | 49066.078 | 49068.665 | 196 | 196 | 0 | 233 | 76 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 194 | 65741.912 | 22917.318 | 194 | 0 | 194 | 235 | 17 | 0 |
| OpenSMT | 0 | 192 | 19014.177 | 18961.011 | 192 | 0 | 192 | 237 | 23 | 0 |
| 2019-SPASS-SATTn | 0 | 190 | 26749.71 | 26728.976 | 190 | 0 | 190 | 239 | 24 | 0 |
| CVC4 | 0 | 187 | 34262.172 | 34270.681 | 187 | 0 | 187 | 242 | 38 | 0 |
| Yices2 | 0 | 180 | 37846.727 | 37846.681 | 180 | 0 | 180 | 249 | 40 | 0 |
| Yices2-fixedn | 0 | 180 | 37986.445 | 37977.666 | 180 | 0 | 180 | 249 | 40 | 0 |
| veriT | 0 | 180 | 40110.027 | 40111.95 | 180 | 0 | 180 | 249 | 52 | 0 |
| z3n | 0 | 180 | 42749.496 | 42720.319 | 180 | 0 | 180 | 249 | 44 | 0 |
| MathSAT5n | 0 | 157 | 67847.769 | 67850.146 | 157 | 0 | 157 | 272 | 76 | 0 |
| SMTInterpol-fixedn | 0 | 156 | 82252.798 | 80270.01 | 156 | 0 | 156 | 273 | 71 | 0 |
| SMTInterpol | 0 | 156 | 82295.031 | 80365.884 | 156 | 0 | 156 | 273 | 72 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-fixedn | 0 | 312 | 3717.279 | 3701.814 | 312 | 181 | 131 | 117 | 117 | 0 | |
| Yices2 | 0 | 311 | 3705.552 | 3701.613 | 311 | 180 | 131 | 118 | 118 | 0 | |
| 2019-SPASS-SATTn | 0 | 306 | 4150.167 | 4116.67 | 306 | 171 | 135 | 123 | 123 | 0 | |
| OpenSMT | 0 | 305 | 4144.049 | 4112.369 | 305 | 155 | 150 | 124 | 124 | 0 | |
| 2019-Par4n | 0 | 294 | 7490.423 | 4341.293 | 294 | 162 | 132 | 135 | 135 | 0 | |
| z3n | 0 | 259 | 4951.217 | 4920.281 | 259 | 146 | 113 | 170 | 170 | 0 | |
| CVC4 | 0 | 258 | 5068.721 | 5061.763 | 258 | 142 | 116 | 171 | 171 | 0 | |
| veriT | 0 | 256 | 4934.931 | 4922.593 | 256 | 133 | 123 | 173 | 173 | 0 | |
| MathSAT5n | 0 | 245 | 4985.407 | 4985.539 | 245 | 141 | 104 | 184 | 184 | 0 | |
| SMTInterpol-fixedn | 0 | 212 | 7316.731 | 6082.116 | 212 | 129 | 83 | 217 | 217 | 0 | |
| SMTInterpol | 0 | 212 | 7311.95 | 6084.702 | 212 | 130 | 82 | 217 | 217 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.