The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTLIRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:04 +0000
Benchmarks: 5520 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 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 4946 | 65830.062 | 65831.728 | 4946 | 0 | 4946 | 574 | 53 | 0 |
| cvc5 | 0 | 4946 | 65913.36 | 65917.818 | 4946 | 0 | 4946 | 574 | 53 | 0 |
| 2020-CVC4n | 0 | 4937 | 52107.636 | 52114.924 | 4937 | 0 | 4937 | 583 | 43 | 0 |
| 2020-Vampiren | 0 | 4645 | 1359830.738 | 1001861.123 | 4645 | 0 | 4645 | 875 | 703 | 0 |
| Vampire - fixedn | 0 | 4456 | 1727186.881 | 1372133.973 | 4456 | 0 | 4456 | 1064 | 1021 | 0 |
| Vampire | 0 | 4445 | 1770017.162 | 1425263.394 | 4445 | 0 | 4445 | 1075 | 1075 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 4946 | 65839.332 | 65829.548 | 4946 | 0 | 4946 | 574 | 53 | 0 |
| cvc5 | 0 | 4946 | 65920.45 | 65915.298 | 4946 | 0 | 4946 | 574 | 53 | 0 |
| 2020-CVC4n | 0 | 4937 | 52113.846 | 52112.554 | 4937 | 0 | 4937 | 583 | 43 | 0 |
| 2020-Vampiren | 0 | 4703 | 1438531.558 | 934262.223 | 4703 | 0 | 4703 | 817 | 603 | 0 |
| Vampire | 0 | 4648 | 1921036.512 | 1281645.076 | 4648 | 0 | 4648 | 872 | 869 | 0 |
| Vampire - fixedn | 0 | 4613 | 1869645.381 | 1269393.177 | 4613 | 0 | 4613 | 907 | 861 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 603 | 0 |
| 2020-CVC4n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 43 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 53 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 869 | 0 |
| Vampire - fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 861 | 0 |
| cvc5 - fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 5520 | 53 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 4946 | 43648.958 | 43639.265 | 4946 | 0 | 4946 | 250 | 324 | 53 | 0 |
| cvc5 | 0 | 4946 | 43713.584 | 43708.08 | 4946 | 0 | 4946 | 250 | 324 | 53 | 0 |
| 2020-CVC4n | 0 | 4937 | 34087.971 | 34086.794 | 4937 | 0 | 4937 | 259 | 324 | 43 | 0 |
| 2020-Vampiren | 0 | 4703 | 1054617.138 | 551971.87 | 4703 | 0 | 4703 | 493 | 324 | 603 | 0 |
| Vampire | 0 | 4648 | 1528636.382 | 892854.626 | 4648 | 0 | 4648 | 548 | 324 | 869 | 0 |
| Vampire - fixedn | 0 | 4613 | 1480845.381 | 880593.177 | 4613 | 0 | 4613 | 583 | 324 | 861 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 4944 | 2030.858 | 2025.365 | 4944 | 0 | 4944 | 576 | 62 | 0 |
| cvc5 - fixedn | 0 | 4943 | 2045.031 | 2034.914 | 4943 | 0 | 4943 | 577 | 63 | 0 |
| 2020-CVC4n | 0 | 4937 | 1510.426 | 1509.135 | 4937 | 0 | 4937 | 583 | 44 | 0 |
| Vampire | 0 | 3762 | 51228.468 | 46462.822 | 3762 | 0 | 3762 | 1758 | 1758 | 0 |
| Vampire - fixedn | 0 | 3737 | 51293.771 | 46429.898 | 3737 | 0 | 3737 | 1783 | 1751 | 0 |
| 2020-Vampiren | 0 | 3340 | 58750.264 | 54966.441 | 3340 | 0 | 3340 | 2180 | 2148 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.