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 2022-08-10 11:17:45 +0000
Benchmarks: 3793 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3793 | 1937.079 | 1943.791 | 3793 | 1560 | 2233 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3792 | 9412.713 | 9388.702 | 3792 | 1560 | 2232 | 1 | 0 | 1 | 0 |
| z3-4.8.17n | 0 | 3791 | 7716.284 | 7690.129 | 3791 | 1560 | 2231 | 2 | 0 | 2 | 0 |
| 2021-z3n | 0 | 3791 | 8114.533 | 8071.614 | 3791 | 1560 | 2231 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 3789 | 11507.618 | 11460.014 | 3789 | 1560 | 2229 | 4 | 0 | 4 | 0 |
| smtinterpol | 0 | 3709 | 135811.47 | 117478.136 | 3709 | 1560 | 2149 | 84 | 0 | 84 | 0 |
| MathSATn | 0 | 3701 | 58308.427 | 58241.501 | 3701 | 1526 | 2175 | 92 | 0 | 44 | 0 |
| veriT | 0 | 3492 | 2944.083 | 2944.569 | 3492 | 1429 | 2063 | 1 | 300 | 1 | 0 |
| OpenSMT-fixedn | 0 | 300 | 454.197 | 439.238 | 300 | 131 | 169 | 0 | 3493 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3793 | 1937.079 | 1943.791 | 3793 | 1560 | 2233 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3792 | 9412.773 | 9388.692 | 3792 | 1560 | 2232 | 1 | 0 | 1 | 0 |
| z3-4.8.17n | 0 | 3791 | 7716.364 | 7690.049 | 3791 | 1560 | 2231 | 2 | 0 | 2 | 0 |
| 2021-z3n | 0 | 3791 | 8114.623 | 8071.484 | 3791 | 1560 | 2231 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 3789 | 11507.998 | 11459.954 | 3789 | 1560 | 2229 | 4 | 0 | 4 | 0 |
| smtinterpol | 0 | 3723 | 144373.36 | 113696.492 | 3723 | 1560 | 2163 | 70 | 0 | 70 | 0 |
| MathSATn | 0 | 3701 | 58313.617 | 58240.021 | 3701 | 1526 | 2175 | 92 | 0 | 44 | 0 |
| veriT | 0 | 3492 | 2944.283 | 2944.539 | 3492 | 1429 | 2063 | 1 | 300 | 1 | 0 |
| OpenSMT-fixedn | 0 | 300 | 454.197 | 439.238 | 300 | 131 | 169 | 0 | 3493 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1560 | 51.53 | 56.94 | 1560 | 1560 | 0 | 0 | 2233 | 0 | 0 |
| z3-4.8.17n | 0 | 1560 | 177.632 | 170.237 | 1560 | 1560 | 0 | 0 | 2233 | 2 | 0 |
| 2021-z3n | 0 | 1560 | 228.434 | 228.736 | 1560 | 1560 | 0 | 0 | 2233 | 2 | 0 |
| OpenSMT | 0 | 1560 | 312.361 | 307.737 | 1560 | 1560 | 0 | 0 | 2233 | 1 | 0 |
| cvc5 | 0 | 1560 | 811.623 | 804.957 | 1560 | 1560 | 0 | 0 | 2233 | 4 | 0 |
| smtinterpol | 0 | 1560 | 4353.679 | 1797.309 | 1560 | 1560 | 0 | 0 | 2233 | 70 | 0 |
| MathSATn | 0 | 1526 | 184.348 | 184.63 | 1526 | 1526 | 0 | 34 | 2233 | 44 | 0 |
| veriT | 0 | 1429 | 140.966 | 140.974 | 1429 | 1429 | 0 | 0 | 2364 | 1 | 0 |
| OpenSMT-fixedn | 0 | 131 | 23.731 | 23.918 | 131 | 131 | 0 | 0 | 3662 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 2233 | 1885.55 | 1886.851 | 2233 | 0 | 2233 | 0 | 1560 | 0 | 0 |
| OpenSMT | 0 | 2232 | 9100.411 | 9080.955 | 2232 | 0 | 2232 | 1 | 1560 | 1 | 0 |
| z3-4.8.17n | 0 | 2231 | 7538.732 | 7519.812 | 2231 | 0 | 2231 | 2 | 1560 | 2 | 0 |
| 2021-z3n | 0 | 2231 | 7886.189 | 7842.748 | 2231 | 0 | 2231 | 2 | 1560 | 2 | 0 |
| cvc5 | 0 | 2229 | 10696.375 | 10654.997 | 2229 | 0 | 2229 | 4 | 1560 | 4 | 0 |
| MathSATn | 0 | 2175 | 58129.269 | 58055.391 | 2175 | 0 | 2175 | 58 | 1560 | 44 | 0 |
| smtinterpol | 0 | 2163 | 140019.681 | 111899.183 | 2163 | 0 | 2163 | 70 | 1560 | 70 | 0 |
| veriT | 0 | 2063 | 2803.317 | 2803.566 | 2063 | 0 | 2063 | 1 | 1729 | 1 | 0 |
| OpenSMT-fixedn | 0 | 169 | 430.467 | 415.321 | 169 | 0 | 169 | 0 | 3624 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3790 | 400.707 | 407.423 | 3790 | 1560 | 2230 | 3 | 0 | 3 | 0 |
| z3-4.8.17n | 0 | 3753 | 2493.715 | 2467.074 | 3753 | 1560 | 2193 | 40 | 0 | 40 | 0 |
| 2021-z3n | 0 | 3751 | 2573.689 | 2530.053 | 3751 | 1559 | 2192 | 42 | 0 | 42 | 0 |
| cvc5 | 0 | 3740 | 3683.89 | 3672.952 | 3740 | 1559 | 2181 | 53 | 0 | 53 | 0 |
| OpenSMT | 0 | 3738 | 3463.974 | 3439.112 | 3738 | 1560 | 2178 | 55 | 0 | 55 | 0 |
| MathSATn | 0 | 3664 | 3204.299 | 3196.704 | 3664 | 1526 | 2138 | 129 | 0 | 81 | 0 |
| smtinterpol | 0 | 3644 | 26464.902 | 13252.28 | 3644 | 1559 | 2085 | 149 | 0 | 149 | 0 |
| veriT | 0 | 3489 | 552.068 | 552.13 | 3489 | 1429 | 2060 | 4 | 300 | 4 | 0 |
| OpenSMT-fixedn | 0 | 297 | 395.676 | 380.702 | 297 | 131 | 166 | 3 | 3493 | 3 | 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.