The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the NRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 93 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 86 | 18125.521 | 17469.201 | 86 | 1 | 85 | 7 | 7 | 0 | |
| Vampire | 0 | 82 | 27315.095 | 26640.396 | 82 | 0 | 82 | 11 | 11 | 0 | |
| 2018-Z3n | 0 | 82 | 27824.522 | 27827.118 | 82 | 1 | 81 | 11 | 11 | 0 | |
| Z3n | 0 | 82 | 27934.787 | 27936.588 | 82 | 1 | 81 | 11 | 11 | 0 | |
| 2018-Vampiren | 0 | 74 | 56842.632 | 48435.42 | 74 | 0 | 74 | 19 | 19 | 0 | |
| CVC4 | 0 | 62 | 69354.415 | 69735.439 | 62 | 0 | 62 | 31 | 29 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 324.94 | 223.03 | 1 | 0 | 1 | 92 | 0 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 317.696 | 223.112 | 0 | 0 | 0 | 93 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 87 | 18560.051 | 16488.711 | 87 | 1 | 86 | 6 | 6 | 0 | |
| Vampire | 0 | 82 | 27315.095 | 26640.396 | 82 | 0 | 82 | 11 | 11 | 0 | |
| 2018-Z3n | 0 | 82 | 27826.612 | 27826.808 | 82 | 1 | 81 | 11 | 11 | 0 | |
| Z3n | 0 | 82 | 27936.017 | 27936.048 | 82 | 1 | 81 | 11 | 11 | 0 | |
| 2018-Vampiren | 0 | 81 | 66169.472 | 38212.969 | 81 | 0 | 81 | 12 | 12 | 0 | |
| CVC4 | 0 | 62 | 69732.905 | 69733.749 | 62 | 0 | 62 | 31 | 29 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 324.94 | 223.03 | 1 | 0 | 1 | 92 | 0 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 317.696 | 223.112 | 0 | 0 | 0 | 93 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 1 | 2400.051 | 2400.052 | 1 | 1 | 0 | 92 | 11 | 0 |
| 2018-Z3n | 0 | 1 | 2400.058 | 2400.058 | 1 | 1 | 0 | 92 | 11 | 0 |
| Par4 | 0 | 1 | 2400.006 | 2400.065 | 1 | 1 | 0 | 92 | 6 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 6.79 | 4.82 | 0 | 0 | 0 | 93 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 6.987 | 5.108 | 0 | 0 | 0 | 93 | 0 | 0 |
| 2018-Vampiren | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 93 | 12 | 0 |
| CVC4 | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 93 | 29 | 0 |
| Vampire | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 93 | 11 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 86 | 16160.045 | 14088.647 | 86 | 0 | 86 | 7 | 6 | 0 |
| Vampire | 0 | 82 | 22515.095 | 21840.396 | 82 | 0 | 82 | 11 | 11 | 0 |
| 2018-Z3n | 0 | 81 | 25426.554 | 25426.75 | 81 | 0 | 81 | 12 | 11 | 0 |
| Z3n | 0 | 81 | 25535.966 | 25535.997 | 81 | 0 | 81 | 12 | 11 | 0 |
| 2018-Vampiren | 0 | 81 | 61369.472 | 33412.969 | 81 | 0 | 81 | 12 | 12 | 0 |
| CVC4 | 0 | 62 | 64932.905 | 64933.749 | 62 | 0 | 62 | 31 | 29 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 317.953 | 217.922 | 1 | 0 | 1 | 92 | 0 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 310.906 | 218.292 | 0 | 0 | 0 | 93 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 85 | 203.011 | 201.212 | 85 | 1 | 84 | 8 | 8 | 0 | |
| Z3n | 0 | 81 | 303.117 | 303.118 | 81 | 1 | 80 | 12 | 12 | 0 | |
| 2018-Z3n | 0 | 81 | 303.592 | 303.598 | 81 | 1 | 80 | 12 | 12 | 0 | |
| Vampire | 0 | 78 | 550.915 | 417.885 | 78 | 0 | 78 | 15 | 15 | 0 | |
| CVC4 | 0 | 62 | 756.462 | 756.441 | 62 | 0 | 62 | 31 | 31 | 0 | |
| 2018-Vampiren | 0 | 61 | 1428.382 | 938.938 | 61 | 0 | 61 | 32 | 32 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 324.94 | 223.03 | 1 | 0 | 1 | 92 | 0 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 317.696 | 223.112 | 0 | 0 | 0 | 93 | 0 | 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.