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 2019-07-23 17:56:09 +0000
Benchmarks: 546 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| SPASS-SATT | Par4 | Par4 | Par4 | Yices 2.6.2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SPASS-SATT | 0 | 527 | 83027.548 | 83035.552 | 527 | 288 | 239 | 19 | 19 | 0 | |
| 2018-CVC4n | 0 | 521 | 137443.771 | 137862.008 | 521 | 282 | 239 | 25 | 25 | 0 | |
| Par4 | 0 | 518 | 148916.734 | 87927.9 | 518 | 286 | 232 | 28 | 28 | 0 | |
| Yices 2.6.2 | 0 | 515 | 121723.739 | 121709.181 | 515 | 280 | 235 | 31 | 31 | 0 | |
| CVC4 | 0 | 515 | 142952.628 | 143325.72 | 515 | 278 | 237 | 31 | 31 | 0 | |
| CVC4-SymBreakn | 0 | 505 | 202131.903 | 202582.243 | 505 | 273 | 232 | 41 | 41 | 0 | |
| veriT | 0 | 495 | 187558.616 | 187547.311 | 495 | 263 | 232 | 51 | 51 | 0 | |
| SMTInterpol | 0 | 486 | 250082.398 | 244020.749 | 486 | 270 | 216 | 60 | 60 | 0 | |
| Z3n | 0 | 447 | 317735.319 | 317772.04 | 447 | 228 | 219 | 99 | 99 | 0 | |
| OpenSMT2 | 0 | 428 | 368259.173 | 368251.522 | 428 | 207 | 221 | 118 | 118 | 0 | |
| Ctrl-Ergo | 0 | 407 | 425587.591 | 356834.914 | 407 | 240 | 167 | 139 | 139 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 535 | 176281.834 | 64378.602 | 535 | 295 | 240 | 11 | 11 | 0 | |
| SPASS-SATT | 0 | 527 | 83031.018 | 83034.962 | 527 | 288 | 239 | 19 | 19 | 0 | |
| 2018-CVC4n | 0 | 521 | 137539.041 | 137860.808 | 521 | 282 | 239 | 25 | 25 | 0 | |
| Yices 2.6.2 | 0 | 515 | 121728.359 | 121708.241 | 515 | 280 | 235 | 31 | 31 | 0 | |
| CVC4 | 0 | 515 | 143132.718 | 143324.46 | 515 | 278 | 237 | 31 | 31 | 0 | |
| CVC4-SymBreakn | 0 | 505 | 202223.173 | 202580.073 | 505 | 273 | 232 | 41 | 41 | 0 | |
| veriT | 0 | 495 | 187567.496 | 187545.431 | 495 | 263 | 232 | 51 | 51 | 0 | |
| SMTInterpol | 0 | 486 | 250082.398 | 244020.749 | 486 | 270 | 216 | 60 | 60 | 0 | |
| Z3n | 0 | 447 | 317760.969 | 317767.14 | 447 | 228 | 219 | 99 | 99 | 0 | |
| Ctrl-Ergo | 0 | 444 | 542492.471 | 319839.014 | 444 | 255 | 189 | 102 | 102 | 0 | |
| OpenSMT2 | 0 | 428 | 368277.243 | 368247.382 | 428 | 207 | 221 | 118 | 118 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 295 | 84047.698 | 26681.626 | 295 | 295 | 0 | 251 | 11 | 0 |
| SPASS-SATT | 0 | 288 | 39922.188 | 39924.218 | 288 | 288 | 0 | 258 | 19 | 0 |
| 2018-CVC4n | 0 | 282 | 86123.945 | 86342.626 | 282 | 282 | 0 | 264 | 25 | 0 |
| Yices 2.6.2 | 0 | 280 | 59070.985 | 59048.791 | 280 | 280 | 0 | 266 | 31 | 0 |
| CVC4 | 0 | 278 | 90831.176 | 90982.437 | 278 | 278 | 0 | 268 | 31 | 0 |
| CVC4-SymBreakn | 0 | 273 | 111881.322 | 112123.711 | 273 | 273 | 0 | 273 | 41 | 0 |
| SMTInterpol | 0 | 270 | 108749.031 | 105455.906 | 270 | 270 | 0 | 276 | 60 | 0 |
| veriT | 0 | 263 | 121596.384 | 121598.964 | 263 | 263 | 0 | 283 | 51 | 0 |
| Ctrl-Ergo | 0 | 255 | 232707.197 | 135859.184 | 255 | 255 | 0 | 291 | 102 | 0 |
| Z3n | 0 | 228 | 211038.291 | 211040.782 | 228 | 228 | 0 | 318 | 99 | 0 |
| OpenSMT2 | 0 | 207 | 267235.482 | 267202.514 | 207 | 207 | 0 | 339 | 118 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 240 | 87434.136 | 32896.976 | 240 | 0 | 240 | 306 | 11 | 0 |
| SPASS-SATT | 0 | 239 | 38308.83 | 38310.744 | 239 | 0 | 239 | 307 | 19 | 0 |
| 2018-CVC4n | 0 | 239 | 46615.097 | 46718.182 | 239 | 0 | 239 | 307 | 25 | 0 |
| CVC4 | 0 | 237 | 47501.542 | 47542.023 | 237 | 0 | 237 | 309 | 31 | 0 |
| Yices 2.6.2 | 0 | 235 | 57857.374 | 57859.45 | 235 | 0 | 235 | 311 | 31 | 0 |
| veriT | 0 | 232 | 61171.112 | 61146.467 | 232 | 0 | 232 | 314 | 51 | 0 |
| CVC4-SymBreakn | 0 | 232 | 85541.851 | 85656.362 | 232 | 0 | 232 | 314 | 41 | 0 |
| OpenSMT2 | 0 | 221 | 96241.761 | 96244.868 | 221 | 0 | 221 | 325 | 118 | 0 |
| Z3n | 0 | 219 | 101922.678 | 101926.357 | 219 | 0 | 219 | 327 | 99 | 0 |
| SMTInterpol | 0 | 216 | 136533.367 | 133764.843 | 216 | 0 | 216 | 330 | 60 | 0 |
| Ctrl-Ergo | 0 | 189 | 304985.274 | 179179.83 | 189 | 0 | 189 | 357 | 102 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 392 | 4793.327 | 4769.744 | 392 | 229 | 163 | 154 | 154 | 0 | |
| Par4 | 0 | 385 | 9154.446 | 5236.39 | 385 | 216 | 169 | 161 | 161 | 0 | |
| SPASS-SATT | 0 | 381 | 5217.609 | 5217.77 | 381 | 219 | 162 | 165 | 165 | 0 | |
| CVC4 | 0 | 332 | 6179.676 | 6177.607 | 332 | 182 | 150 | 214 | 214 | 0 | |
| veriT | 0 | 328 | 6244.773 | 6244.765 | 328 | 174 | 154 | 218 | 218 | 0 | |
| 2018-CVC4n | 0 | 314 | 6471.205 | 6467.019 | 314 | 170 | 144 | 232 | 232 | 0 | |
| Z3n | 0 | 283 | 6937.837 | 6933.156 | 283 | 146 | 137 | 263 | 263 | 0 | |
| OpenSMT2 | 0 | 278 | 7230.787 | 7224.558 | 278 | 144 | 134 | 268 | 268 | 0 | |
| SMTInterpol | 0 | 276 | 9050.096 | 7576.249 | 276 | 167 | 109 | 270 | 270 | 0 | |
| Ctrl-Ergo | 0 | 267 | 10902.263 | 7788.718 | 267 | 149 | 118 | 279 | 279 | 0 | |
| CVC4-SymBreakn | 0 | 261 | 8175.341 | 8167.78 | 261 | 147 | 114 | 285 | 285 | 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.