The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFLRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 541 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 537 | 363.427 | 361.284 | 537 | 320 | 217 | 4 | 4 | 0 |
| SMTInterpol | 0 | 537 | 5012.281 | 2646.254 | 537 | 320 | 217 | 4 | 4 | 0 |
| cvc5 | 0 | 535 | 810.619 | 803.167 | 535 | 318 | 217 | 6 | 6 | 0 |
| OpenSMT | 0 | 532 | 2187.383 | 2187.734 | 532 | 315 | 217 | 9 | 9 | 0 |
| 2022-z3-4.8.17n | 0 | 531 | 1576.298 | 1574.801 | 531 | 316 | 215 | 10 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 537 | 363.427 | 361.284 | 537 | 320 | 217 | 4 | 4 | 0 |
| SMTInterpol | 0 | 537 | 5012.281 | 2646.254 | 537 | 320 | 217 | 4 | 4 | 0 |
| cvc5 | 0 | 535 | 810.619 | 803.167 | 535 | 318 | 217 | 6 | 6 | 0 |
| OpenSMT | 0 | 532 | 2187.383 | 2187.734 | 532 | 315 | 217 | 9 | 9 | 0 |
| 2022-z3-4.8.17n | 0 | 531 | 1576.298 | 1574.801 | 531 | 316 | 215 | 10 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 320 | 344.709 | 345.064 | 320 | 320 | 0 | 3 | 218 | 4 | 0 |
| SMTInterpol | 0 | 320 | 2918.649 | 1639.745 | 320 | 320 | 0 | 3 | 218 | 4 | 0 |
| cvc5 | 0 | 318 | 580.137 | 580.179 | 318 | 318 | 0 | 5 | 218 | 6 | 0 |
| 2022-z3-4.8.17n | 0 | 316 | 1207.336 | 1207.204 | 316 | 316 | 0 | 7 | 218 | 10 | 0 |
| OpenSMT | 0 | 315 | 2103.27 | 2103.589 | 315 | 315 | 0 | 8 | 218 | 9 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 217 | 18.718 | 16.22 | 217 | 0 | 217 | 0 | 324 | 4 | 0 |
| OpenSMT | 0 | 217 | 84.114 | 84.145 | 217 | 0 | 217 | 0 | 324 | 9 | 0 |
| cvc5 | 0 | 217 | 230.483 | 222.988 | 217 | 0 | 217 | 0 | 324 | 6 | 0 |
| SMTInterpol | 0 | 217 | 2093.632 | 1006.509 | 217 | 0 | 217 | 0 | 324 | 4 | 0 |
| 2022-z3-4.8.17n | 0 | 215 | 368.962 | 367.597 | 215 | 0 | 215 | 2 | 324 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 535 | 48.446 | 46.293 | 535 | 318 | 217 | 6 | 6 | 0 |
| cvc5 | 0 | 529 | 160.745 | 153.128 | 529 | 314 | 215 | 12 | 12 | 0 |
| SMTInterpol | 0 | 526 | 2317.157 | 834.751 | 526 | 312 | 214 | 15 | 15 | 0 |
| 2022-z3-4.8.17n | 0 | 522 | 181.069 | 179.132 | 522 | 312 | 210 | 19 | 19 | 0 |
| OpenSMT | 0 | 521 | 330.525 | 330.625 | 521 | 306 | 215 | 20 | 20 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.