The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 3757 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| 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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 3757 | 648.2 | 653.935 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 3757 | 679.032 | 680.382 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3757 | 6559.651 | 6495.544 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3755 | 5303.176 | 5281.273 | 3755 | 1556 | 2199 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 3686 | 32030.259 | 15201.977 | 3686 | 1556 | 2130 | 71 | 0 | 71 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 3757 | 648.2 | 653.935 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 3757 | 679.032 | 680.382 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3757 | 6559.651 | 6495.544 | 3757 | 1556 | 2201 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3755 | 5303.176 | 5281.273 | 3755 | 1556 | 2199 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 3693 | 44480.769 | 21508.286 | 3693 | 1556 | 2137 | 64 | 0 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 1556 | 60.877 | 63.668 | 1556 | 1556 | 0 | 0 | 2201 | 0 | 0 |
| Yices2 | 0 | 1556 | 61.65 | 64.58 | 1556 | 1556 | 0 | 0 | 2201 | 0 | 0 |
| OpenSMT | 0 | 1556 | 354.273 | 353.612 | 1556 | 1556 | 0 | 0 | 2201 | 0 | 0 |
| cvc5 | 0 | 1556 | 543.049 | 537.965 | 1556 | 1556 | 0 | 0 | 2201 | 2 | 0 |
| SMTInterpol | 0 | 1556 | 4351.789 | 1738.445 | 1556 | 1556 | 0 | 0 | 2201 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 2201 | 587.323 | 590.266 | 2201 | 0 | 2201 | 0 | 1556 | 0 | 0 |
| Yices2 | 0 | 2201 | 617.382 | 615.801 | 2201 | 0 | 2201 | 0 | 1556 | 0 | 0 |
| OpenSMT | 0 | 2201 | 6205.378 | 6141.931 | 2201 | 0 | 2201 | 0 | 1556 | 0 | 0 |
| cvc5 | 0 | 2199 | 4760.127 | 4743.307 | 2199 | 0 | 2199 | 2 | 1556 | 2 | 0 |
| SMTInterpol | 0 | 2137 | 40128.981 | 19769.842 | 2137 | 0 | 2137 | 64 | 1556 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 3754 | 252.93 | 258.604 | 3754 | 1556 | 2198 | 3 | 0 | 3 | 0 |
| Yices2 | 0 | 3754 | 260.859 | 262.116 | 3754 | 1556 | 2198 | 3 | 0 | 3 | 0 |
| cvc5 | 0 | 3719 | 2094.352 | 2071.898 | 3719 | 1556 | 2163 | 38 | 0 | 38 | 0 |
| OpenSMT | 0 | 3712 | 2095.441 | 2083.242 | 3712 | 1556 | 2156 | 45 | 0 | 45 | 0 |
| SMTInterpol | 0 | 3611 | 21810.255 | 9155.724 | 3611 | 1556 | 2055 | 146 | 0 | 146 | 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.