The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFLRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 541 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| SMTInterpol | SMTInterpol | SMTInterpol | Yices 2.6.2 | Yices 2.6.2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 541 | 4649.218 | 3214.411 | 541 | 330 | 211 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 540 | 2563.179 | 2563.86 | 540 | 329 | 211 | 1 | 1 | 0 | |
| 2018-Yicesn | 0 | 540 | 2567.292 | 2567.769 | 540 | 329 | 211 | 1 | 1 | 0 | |
| Z3n | 0 | 540 | 2687.28 | 2687.628 | 540 | 329 | 211 | 1 | 1 | 0 | |
| veriT | 0 | 540 | 4614.051 | 4614.139 | 540 | 329 | 211 | 1 | 1 | 0 | |
| CVC4 | 0 | 539 | 5656.556 | 5657.668 | 539 | 328 | 211 | 2 | 2 | 0 | |
| Alt-Ergo | 0 | 200 | 456223.225 | 402187.943 | 200 | 0 | 200 | 341 | 130 | 6 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 541 | 4649.218 | 3214.411 | 541 | 330 | 211 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 540 | 2563.369 | 2563.78 | 540 | 329 | 211 | 1 | 1 | 0 | |
| 2018-Yicesn | 0 | 540 | 2567.502 | 2567.709 | 540 | 329 | 211 | 1 | 1 | 0 | |
| Z3n | 0 | 540 | 2687.56 | 2687.598 | 540 | 329 | 211 | 1 | 1 | 0 | |
| veriT | 0 | 540 | 4614.171 | 4614.109 | 540 | 329 | 211 | 1 | 1 | 0 | |
| CVC4 | 0 | 539 | 5657.446 | 5657.618 | 539 | 328 | 211 | 2 | 2 | 0 | |
| Alt-Ergo | 0 | 201 | 466971.375 | 394859.178 | 201 | 0 | 201 | 340 | 122 | 6 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 330 | 3699.904 | 2760.193 | 330 | 330 | 0 | 211 | 0 | 0 |
| Yices 2.6.2 | 0 | 329 | 2551.4 | 2551.62 | 329 | 329 | 0 | 212 | 1 | 0 |
| 2018-Yicesn | 0 | 329 | 2556.269 | 2556.37 | 329 | 329 | 0 | 212 | 1 | 0 |
| Z3n | 0 | 329 | 2653.588 | 2653.619 | 329 | 329 | 0 | 212 | 1 | 0 |
| veriT | 0 | 329 | 4571.31 | 4571.254 | 329 | 329 | 0 | 212 | 1 | 0 |
| CVC4 | 0 | 328 | 5513.909 | 5514.084 | 328 | 328 | 0 | 213 | 2 | 0 |
| Alt-Ergo | 0 | 0 | 402130.284 | 360578.51 | 0 | 0 | 0 | 541 | 122 | 6 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Yicesn | 0 | 211 | 11.233 | 11.338 | 211 | 0 | 211 | 330 | 1 | 0 |
| Yices 2.6.2 | 0 | 211 | 11.968 | 12.16 | 211 | 0 | 211 | 330 | 1 | 0 |
| Z3n | 0 | 211 | 33.971 | 33.978 | 211 | 0 | 211 | 330 | 1 | 0 |
| veriT | 0 | 211 | 42.861 | 42.854 | 211 | 0 | 211 | 330 | 1 | 0 |
| CVC4 | 0 | 211 | 143.537 | 143.534 | 211 | 0 | 211 | 330 | 2 | 0 |
| SMTInterpol | 0 | 211 | 949.314 | 454.217 | 211 | 0 | 211 | 330 | 0 | 0 |
| Alt-Ergo | 0 | 201 | 64841.091 | 34280.669 | 201 | 0 | 201 | 340 | 122 | 6 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Yicesn | 0 | 539 | 93.714 | 93.912 | 539 | 328 | 211 | 2 | 2 | 0 | |
| Yices 2.6.2 | 0 | 539 | 96.123 | 96.531 | 539 | 328 | 211 | 2 | 2 | 0 | |
| veriT | 0 | 538 | 194.373 | 194.316 | 538 | 327 | 211 | 3 | 3 | 0 | |
| Z3n | 0 | 537 | 206.592 | 206.625 | 537 | 326 | 211 | 4 | 4 | 0 | |
| CVC4 | 0 | 534 | 348.433 | 348.361 | 534 | 324 | 210 | 7 | 7 | 0 | |
| SMTInterpol | 0 | 534 | 1957.696 | 856.737 | 534 | 325 | 209 | 7 | 7 | 0 | |
| Alt-Ergo | 0 | 89 | 15298.058 | 11343.197 | 89 | 0 | 89 | 452 | 402 | 6 |
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.