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 Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 3522 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 | veriT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 3522 | 1068.046 | 1078.476 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 3522 | 1085.832 | 1096.461 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| Yices2 | 0 | 3522 | 1111.369 | 1130.981 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| 2019-Par4n | 0 | 3521 | 1617.048 | 1559.215 | 3521 | 1495 | 2026 | 1 | 1 | 0 |
| veriT | 0 | 3521 | 2544.881 | 2542.089 | 3521 | 1495 | 2026 | 1 | 1 | 0 |
| z3n | 0 | 3520 | 6698.411 | 6692.512 | 3520 | 1495 | 2025 | 2 | 2 | 0 |
| 2020-z3n | 0 | 3520 | 6949.706 | 6934.741 | 3520 | 1495 | 2025 | 2 | 2 | 0 |
| OpenSMT | 0 | 3517 | 13551.975 | 13525.07 | 3517 | 1495 | 2022 | 5 | 5 | 0 |
| cvc5 | 0 | 3517 | 14678.644 | 14608.273 | 3517 | 1495 | 2022 | 5 | 5 | 0 |
| SMTInterpol | 0 | 3478 | 85001.341 | 70595.952 | 3478 | 1495 | 1983 | 44 | 44 | 0 |
| MathSAT5n | 0 | 3433 | 49858.206 | 49875.003 | 3433 | 1455 | 1978 | 89 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 3522 | 1068.046 | 1078.476 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 3522 | 1085.832 | 1096.461 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| Yices2 | 0 | 3522 | 1111.369 | 1130.981 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| 2019-Par4n | 0 | 3522 | 2184.198 | 1242.88 | 3522 | 1495 | 2027 | 0 | 0 | 0 |
| veriT | 0 | 3521 | 2544.941 | 2542.059 | 3521 | 1495 | 2026 | 1 | 1 | 0 |
| z3n | 0 | 3520 | 6698.691 | 6692.472 | 3520 | 1495 | 2025 | 2 | 2 | 0 |
| 2020-z3n | 0 | 3520 | 6949.756 | 6934.721 | 3520 | 1495 | 2025 | 2 | 2 | 0 |
| OpenSMT | 0 | 3517 | 13552.395 | 13524.92 | 3517 | 1495 | 2022 | 5 | 5 | 0 |
| cvc5 | 0 | 3517 | 14678.794 | 14608.183 | 3517 | 1495 | 2022 | 5 | 5 | 0 |
| SMTInterpol | 0 | 3480 | 85491.191 | 70394.752 | 3480 | 1495 | 1985 | 42 | 42 | 0 |
| MathSAT5n | 0 | 3433 | 49898.216 | 49873.453 | 3433 | 1455 | 1978 | 89 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2-fixedn | 0 | 1495 | 54.847 | 60.133 | 1495 | 1495 | 0 | 0 | 2027 | 0 | 0 |
| 2020-Yices2n | 0 | 1495 | 55.118 | 60.499 | 1495 | 1495 | 0 | 0 | 2027 | 0 | 0 |
| Yices2 | 0 | 1495 | 54.996 | 65.404 | 1495 | 1495 | 0 | 0 | 2027 | 0 | 0 |
| 2019-Par4n | 0 | 1495 | 28.13 | 68.538 | 1495 | 1495 | 0 | 0 | 2027 | 0 | 0 |
| veriT | 0 | 1495 | 148.797 | 146.654 | 1495 | 1495 | 0 | 0 | 2027 | 1 | 0 |
| z3n | 0 | 1495 | 297.141 | 297.344 | 1495 | 1495 | 0 | 0 | 2027 | 2 | 0 |
| 2020-z3n | 0 | 1495 | 339.956 | 339.551 | 1495 | 1495 | 0 | 0 | 2027 | 2 | 0 |
| OpenSMT | 0 | 1495 | 646.262 | 640.611 | 1495 | 1495 | 0 | 0 | 2027 | 5 | 0 |
| cvc5 | 0 | 1495 | 648.879 | 645.269 | 1495 | 1495 | 0 | 0 | 2027 | 5 | 0 |
| SMTInterpol | 0 | 1495 | 4397.003 | 1771.949 | 1495 | 1495 | 0 | 0 | 2027 | 42 | 0 |
| MathSAT5n | 0 | 1455 | 168.347 | 168.504 | 1455 | 1455 | 0 | 40 | 2027 | 35 | 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 | 2027 | 1012.928 | 1017.977 | 2027 | 0 | 2027 | 0 | 1495 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 2027 | 1030.984 | 1036.328 | 2027 | 0 | 2027 | 0 | 1495 | 0 | 0 |
| Yices2 | 0 | 2027 | 1056.373 | 1065.576 | 2027 | 0 | 2027 | 0 | 1495 | 0 | 0 |
| 2019-Par4n | 0 | 2027 | 2156.068 | 1174.342 | 2027 | 0 | 2027 | 0 | 1495 | 0 | 0 |
| veriT | 0 | 2026 | 2396.144 | 2395.405 | 2026 | 0 | 2026 | 1 | 1495 | 1 | 0 |
| z3n | 0 | 2025 | 6401.55 | 6395.128 | 2025 | 0 | 2025 | 2 | 1495 | 2 | 0 |
| 2020-z3n | 0 | 2025 | 6609.8 | 6595.17 | 2025 | 0 | 2025 | 2 | 1495 | 2 | 0 |
| OpenSMT | 0 | 2022 | 12906.134 | 12884.309 | 2022 | 0 | 2022 | 5 | 1495 | 5 | 0 |
| cvc5 | 0 | 2022 | 14029.915 | 13962.914 | 2022 | 0 | 2022 | 5 | 1495 | 5 | 0 |
| SMTInterpol | 0 | 1985 | 81094.188 | 68622.803 | 1985 | 0 | 1985 | 42 | 1495 | 42 | 0 |
| MathSAT5n | 0 | 1978 | 49729.869 | 49704.949 | 1978 | 0 | 1978 | 49 | 1495 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3519 | 308.138 | 340.604 | 3519 | 1495 | 2024 | 3 | 3 | 0 |
| veriT | 0 | 3518 | 538.033 | 534.93 | 3518 | 1495 | 2023 | 4 | 4 | 0 |
| 2020-Yices2-fixedn | 0 | 3516 | 374.465 | 385.054 | 3516 | 1495 | 2021 | 6 | 6 | 0 |
| 2020-Yices2n | 0 | 3516 | 374.78 | 385.118 | 3516 | 1495 | 2021 | 6 | 6 | 0 |
| Yices2 | 0 | 3516 | 375.659 | 395.104 | 3516 | 1495 | 2021 | 6 | 6 | 0 |
| 2020-z3n | 0 | 3485 | 2377.881 | 2362.702 | 3485 | 1491 | 1994 | 37 | 37 | 0 |
| z3n | 0 | 3484 | 2276.686 | 2270.001 | 3484 | 1491 | 1993 | 38 | 38 | 0 |
| cvc5 | 0 | 3476 | 3245.698 | 3230.887 | 3476 | 1495 | 1981 | 46 | 46 | 0 |
| OpenSMT | 0 | 3471 | 3671.678 | 3643.532 | 3471 | 1489 | 1982 | 51 | 51 | 0 |
| SMTInterpol | 0 | 3420 | 20469.573 | 9525.572 | 3420 | 1495 | 1925 | 102 | 102 | 0 |
| MathSAT5n | 0 | 3396 | 2825.546 | 2799.825 | 3396 | 1455 | 1941 | 126 | 72 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.