The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFBV logic in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 41 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 32 | 14920.86 | 14923.269 | 32 | 14 | 18 | 9 | 9 | 0 |
| Yices2 | 0 | 32 | 14959.009 | 14960.986 | 32 | 14 | 18 | 9 | 9 | 0 |
| 2020-Yices2-fixedn | 0 | 32 | 15009.491 | 15012.191 | 32 | 14 | 18 | 9 | 9 | 0 |
| MathSAT5n | 0 | 23 | 23680.674 | 23685.845 | 23 | 8 | 15 | 18 | 18 | 0 |
| Bitwuzla | 0 | 22 | 6287.17 | 6289.111 | 22 | 10 | 12 | 19 | 4 | 0 |
| 2020-Bitwuzlan | 0 | 21 | 6287.506 | 6289.624 | 21 | 10 | 11 | 20 | 4 | 0 |
| z3n | 0 | 19 | 27426.257 | 27432.739 | 19 | 8 | 11 | 22 | 22 | 0 |
| cvc5 | 0 | 17 | 26312.716 | 30414.274 | 17 | 5 | 12 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 32 | 14922.05 | 14922.779 | 32 | 14 | 18 | 9 | 9 | 0 |
| Yices2 | 0 | 32 | 14959.999 | 14960.626 | 32 | 14 | 18 | 9 | 9 | 0 |
| 2020-Yices2-fixedn | 0 | 32 | 15011.251 | 15011.931 | 32 | 14 | 18 | 9 | 9 | 0 |
| MathSAT5n | 0 | 23 | 23684.364 | 23684.855 | 23 | 8 | 15 | 18 | 18 | 0 |
| Bitwuzla | 0 | 22 | 6288.6 | 6288.971 | 22 | 10 | 12 | 19 | 4 | 0 |
| 2020-Bitwuzlan | 0 | 21 | 6289.206 | 6289.464 | 21 | 10 | 11 | 20 | 4 | 0 |
| z3n | 0 | 19 | 27431.537 | 27431.679 | 19 | 8 | 11 | 22 | 22 | 0 |
| cvc5 | 0 | 17 | 30404.306 | 30413.084 | 17 | 5 | 12 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 14 | 6631.799 | 6632.278 | 14 | 14 | 0 | 3 | 24 | 9 | 0 |
| Yices2 | 0 | 14 | 6659.361 | 6659.866 | 14 | 14 | 0 | 3 | 24 | 9 | 0 |
| 2020-Yices2-fixedn | 0 | 14 | 6705.969 | 6706.468 | 14 | 14 | 0 | 3 | 24 | 9 | 0 |
| Bitwuzla | 0 | 10 | 1440.22 | 1440.536 | 10 | 10 | 0 | 7 | 24 | 4 | 0 |
| 2020-Bitwuzlan | 0 | 10 | 1447.997 | 1448.176 | 10 | 10 | 0 | 7 | 24 | 4 | 0 |
| MathSAT5n | 0 | 8 | 10989.246 | 10989.287 | 8 | 8 | 0 | 9 | 24 | 18 | 0 |
| z3n | 0 | 8 | 11765.453 | 11765.577 | 8 | 8 | 0 | 9 | 24 | 22 | 0 |
| cvc5 | 0 | 5 | 14872.191 | 14872.252 | 5 | 5 | 0 | 12 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 18 | 3490.25 | 3490.501 | 18 | 0 | 18 | 2 | 21 | 9 | 0 |
| Yices2 | 0 | 18 | 3500.638 | 3500.76 | 18 | 0 | 18 | 2 | 21 | 9 | 0 |
| 2020-Yices2-fixedn | 0 | 18 | 3505.282 | 3505.463 | 18 | 0 | 18 | 2 | 21 | 9 | 0 |
| MathSAT5n | 0 | 15 | 7895.118 | 7895.568 | 15 | 0 | 15 | 5 | 21 | 18 | 0 |
| Bitwuzla | 0 | 12 | 48.379 | 48.435 | 12 | 0 | 12 | 8 | 21 | 4 | 0 |
| cvc5 | 0 | 12 | 10732.115 | 10740.832 | 12 | 0 | 12 | 8 | 21 | 24 | 0 |
| 2020-Bitwuzlan | 0 | 11 | 41.209 | 41.287 | 11 | 0 | 11 | 9 | 21 | 4 | 0 |
| z3n | 0 | 11 | 10866.084 | 10866.103 | 11 | 0 | 11 | 9 | 21 | 22 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 23 | 472.987 | 473.023 | 23 | 8 | 15 | 18 | 18 | 0 |
| 2020-Yices2-fixedn | 0 | 23 | 473.123 | 473.16 | 23 | 8 | 15 | 18 | 18 | 0 |
| Yices2 | 0 | 23 | 473.761 | 473.822 | 23 | 8 | 15 | 18 | 18 | 0 |
| Bitwuzla | 0 | 18 | 212.69 | 212.768 | 18 | 7 | 11 | 23 | 8 | 0 |
| 2020-Bitwuzlan | 0 | 17 | 200.547 | 200.67 | 17 | 7 | 10 | 24 | 8 | 0 |
| MathSAT5n | 0 | 17 | 609.577 | 609.584 | 17 | 6 | 11 | 24 | 24 | 0 |
| cvc5 | 0 | 14 | 687.586 | 687.584 | 14 | 3 | 11 | 27 | 27 | 0 |
| z3n | 0 | 14 | 696.666 | 696.681 | 14 | 4 | 10 | 27 | 27 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.