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 2021-07-18 17:29:06 +0000
Benchmarks: 4229 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 4022 | 344584.895 | 344636.271 | 4022 | 1718 | 2304 | 207 | 0 | 207 | 0 |
| cvc5 | 0 | 4009 | 373000.802 | 372991.654 | 4009 | 1715 | 2294 | 220 | 0 | 220 | 0 |
| 2020-z3n | 0 | 3920 | 184851.546 | 184851.611 | 3920 | 1705 | 2215 | 106 | 203 | 106 | 0 |
| 2020-Yices2n | 0 | 3822 | 1072.215 | 1084.122 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 3822 | 1089.993 | 1102.062 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| Yices2 | 0 | 3822 | 1115.685 | 1137.975 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| SMTInterpol | 0 | 3817 | 546477.94 | 530239.151 | 3817 | 1670 | 2147 | 412 | 0 | 412 | 0 |
| MathSAT5n | 0 | 3733 | 49878.922 | 49895.774 | 3733 | 1624 | 2109 | 89 | 407 | 35 | 0 |
| 2019-Par4n | 0 | 3521 | 1617.048 | 1559.215 | 3521 | 1495 | 2026 | 1 | 707 | 1 | 0 |
| veriT | 0 | 3521 | 2544.881 | 2542.089 | 3521 | 1495 | 2026 | 1 | 707 | 1 | 0 |
| OpenSMT | 0 | 3517 | 13551.975 | 13525.07 | 3517 | 1495 | 2022 | 5 | 707 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 4022 | 344609.165 | 344628.691 | 4022 | 1718 | 2304 | 207 | 0 | 207 | 0 |
| cvc5 | 0 | 4009 | 373038.902 | 372982.584 | 4009 | 1715 | 2294 | 220 | 0 | 220 | 0 |
| 2020-z3n | 0 | 3920 | 184860.746 | 184848.161 | 3920 | 1705 | 2215 | 106 | 203 | 106 | 0 |
| SMTInterpol | 0 | 3825 | 547427.64 | 529767.111 | 3825 | 1670 | 2155 | 404 | 0 | 404 | 0 |
| 2020-Yices2n | 0 | 3822 | 1072.215 | 1084.122 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 3822 | 1089.993 | 1102.062 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| Yices2 | 0 | 3822 | 1115.685 | 1137.975 | 3822 | 1664 | 2158 | 0 | 407 | 0 | 0 |
| MathSAT5n | 0 | 3733 | 49918.932 | 49894.224 | 3733 | 1624 | 2109 | 89 | 407 | 35 | 0 |
| 2019-Par4n | 0 | 3522 | 2184.198 | 1242.88 | 3522 | 1495 | 2027 | 0 | 707 | 0 | 0 |
| veriT | 0 | 3521 | 2544.941 | 2542.059 | 3521 | 1495 | 2026 | 1 | 707 | 1 | 0 |
| OpenSMT | 0 | 3517 | 13552.395 | 13524.92 | 3517 | 1495 | 2022 | 5 | 707 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1718 | 210655.534 | 210658.266 | 1718 | 1718 | 0 | 152 | 2359 | 207 | 0 |
| cvc5 | 0 | 1715 | 210278.655 | 210279.867 | 1715 | 1715 | 0 | 155 | 2359 | 220 | 0 |
| 2020-z3n | 0 | 1705 | 95858.793 | 95860.474 | 1705 | 1705 | 0 | 62 | 2462 | 106 | 0 |
| SMTInterpol | 0 | 1670 | 244542.387 | 241847.553 | 1670 | 1670 | 0 | 200 | 2359 | 404 | 0 |
| 2020-Yices2-fixedn | 0 | 1664 | 55.791 | 62.207 | 1664 | 1664 | 0 | 0 | 2565 | 0 | 0 |
| 2020-Yices2n | 0 | 1664 | 56.098 | 62.635 | 1664 | 1664 | 0 | 0 | 2565 | 0 | 0 |
| Yices2 | 0 | 1664 | 55.974 | 68.367 | 1664 | 1664 | 0 | 0 | 2565 | 0 | 0 |
| MathSAT5n | 0 | 1624 | 176.418 | 176.585 | 1624 | 1624 | 0 | 40 | 2565 | 35 | 0 |
| 2019-Par4n | 0 | 1495 | 28.13 | 68.538 | 1495 | 1495 | 0 | 0 | 2734 | 0 | 0 |
| veriT | 0 | 1495 | 148.797 | 146.654 | 1495 | 1495 | 0 | 0 | 2734 | 1 | 0 |
| OpenSMT | 0 | 1495 | 646.262 | 640.611 | 1495 | 1495 | 0 | 0 | 2734 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 2304 | 133953.631 | 133970.425 | 2304 | 0 | 2304 | 55 | 1870 | 207 | 0 |
| cvc5 | 0 | 2294 | 162760.248 | 162702.717 | 2294 | 0 | 2294 | 65 | 1870 | 220 | 0 |
| 2020-z3n | 0 | 2215 | 89001.953 | 88987.686 | 2215 | 0 | 2215 | 44 | 1970 | 106 | 0 |
| 2020-Yices2n | 0 | 2158 | 1016.117 | 1021.488 | 2158 | 0 | 2158 | 0 | 2071 | 0 | 0 |
| 2020-Yices2-fixedn | 0 | 2158 | 1034.201 | 1039.855 | 2158 | 0 | 2158 | 0 | 2071 | 0 | 0 |
| Yices2 | 0 | 2158 | 1059.711 | 1069.608 | 2158 | 0 | 2158 | 0 | 2071 | 0 | 0 |
| SMTInterpol | 0 | 2155 | 302885.254 | 287919.558 | 2155 | 0 | 2155 | 204 | 1870 | 404 | 0 |
| MathSAT5n | 0 | 2109 | 49742.514 | 49717.639 | 2109 | 0 | 2109 | 49 | 2071 | 35 | 0 |
| 2019-Par4n | 0 | 2027 | 2156.068 | 1174.342 | 2027 | 0 | 2027 | 0 | 2202 | 0 | 0 |
| veriT | 0 | 2026 | 2396.144 | 2395.405 | 2026 | 0 | 2026 | 1 | 2202 | 1 | 0 |
| OpenSMT | 0 | 2022 | 12906.134 | 12884.309 | 2022 | 0 | 2022 | 5 | 2202 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Yices2-fixedn | 0 | 3816 | 378.626 | 390.655 | 3816 | 1664 | 2152 | 6 | 407 | 6 | 0 |
| 2020-Yices2n | 0 | 3816 | 378.949 | 390.764 | 3816 | 1664 | 2152 | 6 | 407 | 6 | 0 |
| Yices2 | 0 | 3816 | 379.975 | 402.098 | 3816 | 1664 | 2152 | 6 | 407 | 6 | 0 |
| z3n | 0 | 3793 | 11883.304 | 11876.667 | 3793 | 1667 | 2126 | 436 | 0 | 436 | 0 |
| 2020-z3n | 0 | 3790 | 7196.658 | 7178.721 | 3790 | 1663 | 2127 | 236 | 203 | 236 | 0 |
| cvc5 | 0 | 3781 | 12982.998 | 12968.146 | 3781 | 1670 | 2111 | 448 | 0 | 448 | 0 |
| SMTInterpol | 0 | 3727 | 30621.031 | 19364.375 | 3727 | 1670 | 2057 | 502 | 0 | 502 | 0 |
| MathSAT5n | 0 | 3696 | 2846.261 | 2820.596 | 3696 | 1624 | 2072 | 126 | 407 | 72 | 0 |
| 2019-Par4n | 0 | 3519 | 308.138 | 340.604 | 3519 | 1495 | 2024 | 3 | 707 | 3 | 0 |
| veriT | 0 | 3518 | 538.033 | 534.93 | 3518 | 1495 | 2023 | 4 | 707 | 4 | 0 |
| OpenSMT | 0 | 3471 | 3671.678 | 3643.532 | 3471 | 1489 | 1982 | 51 | 707 | 51 | 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.