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 2022-08-10 11:17:45 +0000
Benchmarks: 3493 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 | 3493 | 1931.565 | 1937.043 | 3493 | 1429 | 2064 | 0 | 0 | 0 |
| veriT | 0 | 3492 | 2944.083 | 2944.569 | 3492 | 1429 | 2063 | 1 | 1 | 0 |
| OpenSMT | 0 | 3492 | 9125.211 | 9101.913 | 3492 | 1429 | 2063 | 1 | 1 | 0 |
| z3-4.8.17n | 0 | 3491 | 7690.84 | 7665.183 | 3491 | 1429 | 2062 | 2 | 2 | 0 |
| 2021-z3n | 0 | 3491 | 8087.43 | 8047.73 | 3491 | 1429 | 2062 | 2 | 2 | 0 |
| cvc5 | 0 | 3489 | 11304.871 | 11257.304 | 3489 | 1429 | 2060 | 4 | 4 | 0 |
| smtinterpol | 0 | 3409 | 134865.74 | 117102.752 | 3409 | 1429 | 1980 | 84 | 84 | 0 |
| MathSATn | 0 | 3401 | 58281.757 | 58214.758 | 3401 | 1395 | 2006 | 92 | 44 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3493 | 1931.565 | 1937.043 | 3493 | 1429 | 2064 | 0 | 0 | 0 |
| veriT | 0 | 3492 | 2944.283 | 2944.539 | 3492 | 1429 | 2063 | 1 | 1 | 0 |
| OpenSMT | 0 | 3492 | 9125.271 | 9101.903 | 3492 | 1429 | 2063 | 1 | 1 | 0 |
| z3-4.8.17n | 0 | 3491 | 7690.92 | 7665.103 | 3491 | 1429 | 2062 | 2 | 2 | 0 |
| 2021-z3n | 0 | 3491 | 8087.52 | 8047.6 | 3491 | 1429 | 2062 | 2 | 2 | 0 |
| cvc5 | 0 | 3489 | 11305.251 | 11257.244 | 3489 | 1429 | 2060 | 4 | 4 | 0 |
| smtinterpol | 0 | 3423 | 143427.63 | 113321.108 | 3423 | 1429 | 1994 | 70 | 70 | 0 |
| MathSATn | 0 | 3401 | 58286.947 | 58213.278 | 3401 | 1395 | 2006 | 92 | 44 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1429 | 50.65 | 55.181 | 1429 | 1429 | 0 | 0 | 2064 | 0 | 0 |
| veriT | 0 | 1429 | 140.966 | 140.974 | 1429 | 1429 | 0 | 0 | 2064 | 1 | 0 |
| z3-4.8.17n | 0 | 1429 | 171.536 | 164.366 | 1429 | 1429 | 0 | 0 | 2064 | 2 | 0 |
| 2021-z3n | 0 | 1429 | 223.067 | 223.359 | 1429 | 1429 | 0 | 0 | 2064 | 2 | 0 |
| OpenSMT | 0 | 1429 | 288.077 | 284.292 | 1429 | 1429 | 0 | 0 | 2064 | 1 | 0 |
| cvc5 | 0 | 1429 | 793.998 | 787.377 | 1429 | 1429 | 0 | 0 | 2064 | 4 | 0 |
| smtinterpol | 0 | 1429 | 4192.859 | 1721.253 | 1429 | 1429 | 0 | 0 | 2064 | 70 | 0 |
| MathSATn | 0 | 1395 | 176.137 | 176.392 | 1395 | 1395 | 0 | 34 | 2064 | 44 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 2064 | 1880.915 | 1881.862 | 2064 | 0 | 2064 | 0 | 1429 | 0 | 0 |
| veriT | 0 | 2063 | 2803.317 | 2803.566 | 2063 | 0 | 2063 | 1 | 1429 | 1 | 0 |
| OpenSMT | 0 | 2063 | 8837.195 | 8817.611 | 2063 | 0 | 2063 | 1 | 1429 | 1 | 0 |
| z3-4.8.17n | 0 | 2062 | 7519.385 | 7500.737 | 2062 | 0 | 2062 | 2 | 1429 | 2 | 0 |
| 2021-z3n | 0 | 2062 | 7864.453 | 7824.241 | 2062 | 0 | 2062 | 2 | 1429 | 2 | 0 |
| cvc5 | 0 | 2060 | 10511.252 | 10469.868 | 2060 | 0 | 2060 | 4 | 1429 | 4 | 0 |
| MathSATn | 0 | 2006 | 58110.811 | 58036.886 | 2006 | 0 | 2006 | 58 | 1429 | 44 | 0 |
| smtinterpol | 0 | 1994 | 139234.771 | 111599.855 | 1994 | 0 | 1994 | 70 | 1429 | 70 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3490 | 395.192 | 400.675 | 3490 | 1429 | 2061 | 3 | 3 | 0 |
| veriT | 0 | 3489 | 552.068 | 552.13 | 3489 | 1429 | 2060 | 4 | 4 | 0 |
| z3-4.8.17n | 0 | 3453 | 2468.271 | 2442.128 | 3453 | 1429 | 2024 | 40 | 40 | 0 |
| 2021-z3n | 0 | 3451 | 2546.585 | 2506.169 | 3451 | 1428 | 2023 | 42 | 42 | 0 |
| cvc5 | 0 | 3442 | 3496.602 | 3485.724 | 3442 | 1428 | 2014 | 51 | 51 | 0 |
| OpenSMT | 0 | 3439 | 3182.366 | 3158.222 | 3439 | 1429 | 2010 | 54 | 54 | 0 |
| MathSATn | 0 | 3364 | 3177.629 | 3169.961 | 3364 | 1395 | 1969 | 129 | 81 | 0 |
| smtinterpol | 0 | 3344 | 25519.172 | 12876.896 | 3344 | 1428 | 1916 | 149 | 149 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.