The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UF logic in the Model Validation Track.
Page generated on 2022-08-10 11:19:11 +0000
Benchmarks: 1571 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| Yices2 | 0 | 1571 | 69.015 | 74.425 | 0 | 0 |
| 2021-Yices2 model-validationn | 0 | 1571 | 70.273 | 72.563 | 0 | 0 |
| z3-4.8.17n | 0 | 1571 | 197.3 | 178.391 | 0 | 0 |
| cvc5 | 0 | 1571 | 797.319 | 801.265 | 0 | 0 |
| smtinterpol | 0 | 1571 | 4560.974 | 2000.302 | 0 | 0 |
| OpenSMT | 0 | 1551 | 297.822 | 305.319 | 0 | 0 |
| MathSATn | 0 | 636 | 230.228 | 226.871 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| 2021-Yices2 model-validationn | 0 | 1571 | 70.273 | 72.563 | 0 | 0 |
| Yices2 | 0 | 1571 | 69.015 | 74.425 | 0 | 0 |
| z3-4.8.17n | 0 | 1571 | 197.3 | 178.391 | 0 | 0 |
| cvc5 | 0 | 1571 | 797.319 | 801.265 | 0 | 0 |
| smtinterpol | 0 | 1571 | 4560.974 | 2000.302 | 0 | 0 |
| OpenSMT | 0 | 1551 | 297.822 | 305.319 | 0 | 0 |
| MathSATn | 0 | 636 | 230.228 | 226.871 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.