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 2022-08-10 11:17:44 +0000
Benchmarks: 38 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 | 27 | 15250.847 | 15253.904 | 27 | 12 | 15 | 11 | 11 | 0 |
| z3-4.8.17n | 0 | 21 | 20695.22 | 20700.52 | 21 | 7 | 14 | 17 | 16 | 0 |
| MathSATn | 0 | 20 | 24441.721 | 24446.703 | 20 | 8 | 12 | 18 | 18 | 0 |
| Bitwuzla | 0 | 19 | 6076.237 | 6078.585 | 19 | 10 | 9 | 19 | 4 | 0 |
| 2020-Bitwuzlan | 0 | 18 | 5415.101 | 5416.716 | 18 | 10 | 8 | 20 | 4 | 0 |
| cvc5 | 0 | 14 | 29134.137 | 30267.059 | 14 | 5 | 9 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 27 | 15253.197 | 15253.454 | 27 | 12 | 15 | 11 | 11 | 0 |
| z3-4.8.17n | 0 | 21 | 20699.52 | 20699.79 | 21 | 7 | 14 | 17 | 16 | 0 |
| MathSATn | 0 | 20 | 24445.111 | 24445.673 | 20 | 8 | 12 | 18 | 18 | 0 |
| Bitwuzla | 0 | 19 | 6077.877 | 6078.335 | 19 | 10 | 9 | 19 | 4 | 0 |
| 2020-Bitwuzlan | 0 | 18 | 5416.181 | 5416.506 | 18 | 10 | 8 | 20 | 4 | 0 |
| cvc5 | 0 | 14 | 30257.597 | 30265.629 | 14 | 5 | 9 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 12 | 7625.505 | 7625.688 | 12 | 12 | 0 | 5 | 21 | 11 | 0 |
| 2020-Bitwuzlan | 0 | 10 | 575.176 | 575.414 | 10 | 10 | 0 | 7 | 21 | 4 | 0 |
| Bitwuzla | 0 | 10 | 1237.194 | 1237.604 | 10 | 10 | 0 | 7 | 21 | 4 | 0 |
| MathSATn | 0 | 8 | 11018.373 | 11018.415 | 8 | 8 | 0 | 9 | 21 | 18 | 0 |
| z3-4.8.17n | 0 | 7 | 12399.535 | 12399.592 | 7 | 7 | 0 | 10 | 21 | 16 | 0 |
| cvc5 | 0 | 5 | 14714.534 | 14714.552 | 5 | 5 | 0 | 12 | 21 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 15 | 2827.692 | 2827.766 | 15 | 0 | 15 | 2 | 21 | 11 | 0 |
| z3-4.8.17n | 0 | 14 | 4430.984 | 4431.185 | 14 | 0 | 14 | 3 | 21 | 16 | 0 |
| MathSATn | 0 | 12 | 8626.738 | 8627.258 | 12 | 0 | 12 | 5 | 21 | 18 | 0 |
| Bitwuzla | 0 | 9 | 40.683 | 40.731 | 9 | 0 | 9 | 8 | 21 | 4 | 0 |
| cvc5 | 0 | 9 | 10743.063 | 10751.077 | 9 | 0 | 9 | 8 | 21 | 24 | 0 |
| 2020-Bitwuzlan | 0 | 8 | 41.005 | 41.092 | 8 | 0 | 8 | 9 | 21 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 20 | 464.835 | 464.868 | 20 | 8 | 12 | 18 | 18 | 0 |
| Bitwuzla | 0 | 15 | 209.79 | 209.819 | 15 | 7 | 8 | 23 | 8 | 0 |
| 2020-Bitwuzlan | 0 | 14 | 200.44 | 200.585 | 14 | 7 | 7 | 24 | 8 | 0 |
| MathSATn | 0 | 14 | 629.779 | 629.808 | 14 | 6 | 8 | 24 | 24 | 0 |
| z3-4.8.17n | 0 | 12 | 688.3 | 688.299 | 12 | 4 | 8 | 26 | 26 | 0 |
| cvc5 | 0 | 11 | 692.142 | 692.142 | 11 | 4 | 7 | 27 | 27 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.