The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFNRA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 27 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 25 | 3254.707 | 3246.236 | 25 | 23 | 2 | 2 | 2 | 0 |
| Yices2 | 0 | 24 | 10789.761 | 10790.913 | 24 | 22 | 2 | 3 | 3 | 0 |
| cvc5 | 0 | 20 | 12066.491 | 12067.628 | 20 | 18 | 2 | 7 | 7 | 0 |
| 2020-CVC4n | 0 | 15 | 16005.036 | 16004.903 | 15 | 13 | 2 | 12 | 12 | 0 |
| MathSATn | 0 | 9 | 20492.717 | 20495.058 | 9 | 7 | 2 | 18 | 17 | 0 |
| smtinterpol | 0 | 1 | 15.393 | 10.231 | 1 | 1 | 0 | 26 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 31196.498 | 31200.824 | 1 | 1 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 25 | 3254.757 | 3246.166 | 25 | 23 | 2 | 2 | 2 | 0 |
| Yices2 | 0 | 24 | 10790.131 | 10790.843 | 24 | 22 | 2 | 3 | 3 | 0 |
| cvc5 | 0 | 20 | 12067.051 | 12067.418 | 20 | 18 | 2 | 7 | 7 | 0 |
| 2020-CVC4n | 0 | 15 | 16007.086 | 16004.333 | 15 | 13 | 2 | 12 | 12 | 0 |
| MathSATn | 0 | 9 | 20494.447 | 20494.458 | 9 | 7 | 2 | 18 | 17 | 0 |
| smtinterpol | 0 | 1 | 15.393 | 10.231 | 1 | 1 | 0 | 26 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 31200.008 | 31200.014 | 1 | 1 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 23 | 2054.43 | 2045.842 | 23 | 23 | 0 | 1 | 3 | 2 | 0 |
| Yices2 | 0 | 22 | 9589.753 | 9590.465 | 22 | 22 | 0 | 2 | 3 | 3 | 0 |
| cvc5 | 0 | 18 | 10858.213 | 10858.581 | 18 | 18 | 0 | 6 | 3 | 7 | 0 |
| 2020-CVC4n | 0 | 13 | 14797.23 | 14797.717 | 13 | 13 | 0 | 11 | 3 | 12 | 0 |
| MathSATn | 0 | 7 | 19294.202 | 19294.212 | 7 | 7 | 0 | 17 | 3 | 17 | 0 |
| smtinterpol | 0 | 1 | 13.634 | 9.061 | 1 | 1 | 0 | 23 | 3 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 27600.008 | 27600.014 | 1 | 1 | 0 | 23 | 3 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| MathSATn | 0 | 2 | 0.246 | 0.246 | 2 | 0 | 2 | 0 | 25 | 17 | 0 |
| z3-4.8.17n | 0 | 2 | 0.328 | 0.324 | 2 | 0 | 2 | 0 | 25 | 2 | 0 |
| Yices2 | 0 | 2 | 0.378 | 0.378 | 2 | 0 | 2 | 0 | 25 | 3 | 0 |
| 2020-CVC4n | 0 | 2 | 9.857 | 6.616 | 2 | 0 | 2 | 0 | 25 | 12 | 0 |
| cvc5 | 0 | 2 | 8.838 | 8.838 | 2 | 0 | 2 | 0 | 25 | 7 | 0 |
| smtinterpol | 0 | 0 | 1.18 | 0.781 | 0 | 0 | 0 | 2 | 25 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 2 | 25 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 20 | 360.341 | 351.687 | 20 | 18 | 2 | 7 | 7 | 0 |
| MathSATn | 0 | 8 | 500.388 | 500.394 | 8 | 6 | 2 | 19 | 18 | 0 |
| Yices2 | 0 | 6 | 521.669 | 521.673 | 6 | 4 | 2 | 21 | 21 | 0 |
| 2020-CVC4n | 0 | 4 | 570.483 | 567.248 | 4 | 2 | 2 | 23 | 23 | 0 |
| cvc5 | 0 | 3 | 584.874 | 584.873 | 3 | 1 | 2 | 24 | 24 | 0 |
| smtinterpol | 0 | 1 | 15.393 | 10.231 | 1 | 1 | 0 | 26 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 624.008 | 624.014 | 1 | 1 | 0 | 26 | 26 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.