The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTLIRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 3900 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 2948 | 6185.798 | 6189.835 | 2948 | 34 | 2914 | 952 | 5 | 0 |
| cvc5 | 0 | 2948 | 9953.375 | 9954.644 | 2948 | 34 | 2914 | 952 | 8 | 0 |
| cvc5 - fixedn | 0 | 2948 | 9961.086 | 9964.652 | 2948 | 34 | 2914 | 952 | 8 | 0 |
| Vampire | 0 | 2904 | 1443375.364 | 1265002.982 | 2904 | 10 | 2894 | 996 | 995 | 0 |
| Vampire - fixedn | 0 | 2885 | 1421794.014 | 1259131.459 | 2885 | 10 | 2875 | 1015 | 993 | 0 |
| iProver | 0 | 2550 | 1640227.341 | 1623164.17 | 2550 | 0 | 2550 | 1350 | 1346 | 0 |
| 2020-Vampiren | 14 | 3243 | 865876.64 | 775803.14 | 3243 | 4 | 3239 | 657 | 608 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 2948 | 6188.348 | 6189.635 | 2948 | 34 | 2914 | 952 | 5 | 0 |
| cvc5 | 0 | 2948 | 9956.135 | 9954.284 | 2948 | 34 | 2914 | 952 | 8 | 0 |
| cvc5 - fixedn | 0 | 2948 | 9965.486 | 9964.352 | 2948 | 34 | 2914 | 952 | 8 | 0 |
| Vampire | 0 | 2919 | 1491739.104 | 1256239.247 | 2919 | 10 | 2909 | 981 | 980 | 0 |
| Vampire - fixedn | 0 | 2898 | 1449575.174 | 1252173.485 | 2898 | 10 | 2888 | 1002 | 980 | 0 |
| iProver | 0 | 2567 | 1664952.191 | 1614173.201 | 2567 | 0 | 2567 | 1333 | 1329 | 0 |
| 2020-Vampiren | 14 | 3253 | 876036.06 | 768647.166 | 3253 | 4 | 3249 | 647 | 597 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 34 | 0.75 | 0.727 | 34 | 34 | 0 | 5 | 3861 | 8 | 0 |
| cvc5 - fixedn | 0 | 34 | 0.772 | 0.777 | 34 | 34 | 0 | 5 | 3861 | 8 | 0 |
| 2020-CVC4n | 0 | 34 | 0.687 | 0.784 | 34 | 34 | 0 | 5 | 3861 | 5 | 0 |
| Vampire | 0 | 10 | 41962.327 | 35776.52 | 10 | 10 | 0 | 29 | 3861 | 980 | 0 |
| Vampire - fixedn | 0 | 10 | 38204.91 | 35778.457 | 10 | 10 | 0 | 29 | 3861 | 980 | 0 |
| 2020-Vampiren | 0 | 4 | 25986.69 | 25439.979 | 4 | 4 | 0 | 35 | 3861 | 597 | 0 |
| iProver | 0 | 0 | 46800.0 | 46800.0 | 0 | 0 | 0 | 39 | 3861 | 1329 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 2914 | 6168.677 | 6169.666 | 2914 | 0 | 2914 | 387 | 599 | 5 | 0 |
| cvc5 | 0 | 2914 | 7536.21 | 7534.652 | 2914 | 0 | 2914 | 387 | 599 | 8 | 0 |
| cvc5 - fixedn | 0 | 2914 | 7545.345 | 7544.229 | 2914 | 0 | 2914 | 387 | 599 | 8 | 0 |
| Vampire | 0 | 2909 | 759775.747 | 548484.907 | 2909 | 0 | 2909 | 392 | 599 | 980 | 0 |
| Vampire - fixedn | 0 | 2888 | 739370.264 | 544395.028 | 2888 | 0 | 2888 | 413 | 599 | 980 | 0 |
| iProver | 0 | 2567 | 946152.191 | 895373.201 | 2567 | 0 | 2567 | 734 | 599 | 1329 | 0 |
| 2020-Vampiren | 14 | 3249 | 178049.37 | 71207.188 | 3249 | 0 | 3249 | 52 | 599 | 597 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 2948 | 308.348 | 309.635 | 2948 | 34 | 2914 | 952 | 5 | 0 |
| cvc5 | 0 | 2947 | 396.826 | 394.877 | 2947 | 34 | 2913 | 953 | 9 | 0 |
| cvc5 - fixedn | 0 | 2947 | 398.851 | 397.642 | 2947 | 34 | 2913 | 953 | 9 | 0 |
| iProver | 0 | 2505 | 40967.204 | 36814.134 | 2505 | 0 | 2505 | 1395 | 1395 | 0 |
| Vampire | 0 | 2314 | 39896.454 | 39015.384 | 2314 | 0 | 2314 | 1586 | 1586 | 0 |
| Vampire - fixedn | 0 | 2296 | 39988.04 | 39089.678 | 2296 | 0 | 2296 | 1604 | 1588 | 0 |
| 2020-Vampiren | 13 | 2764 | 43781.788 | 36126.874 | 2764 | 0 | 2764 | 1136 | 1097 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.