The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFNRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 26 | 4543.262 | 2873.807 | 26 | 24 | 2 | 1 | 1 | 0 | |
| Yices2 | 0 | 25 | 10360.485 | 10361.347 | 25 | 23 | 2 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 25 | 10528.792 | 10529.826 | 25 | 23 | 2 | 2 | 2 | 0 | |
| z3n | 0 | 21 | 460.452 | 443.592 | 21 | 19 | 2 | 6 | 0 | 0 | |
| CVC4 | 0 | 12 | 18502.769 | 18507.039 | 12 | 10 | 2 | 15 | 14 | 0 | |
| MathSAT5n | 0 | 8 | 21742.699 | 21745.121 | 8 | 6 | 2 | 19 | 18 | 0 | |
| veriT+raSAT+Redlog | 0 | 1 | 31193.657 | 31200.89 | 1 | 1 | 0 | 26 | 26 | 0 | |
| Alt-Ergo | 0 | 0 | 31200.187 | 31200.067 | 0 | 0 | 0 | 27 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 26 | 4543.262 | 2873.807 | 26 | 24 | 2 | 1 | 1 | 0 | |
| Yices2 | 0 | 25 | 10360.715 | 10361.307 | 25 | 23 | 2 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 25 | 10528.992 | 10529.796 | 25 | 23 | 2 | 2 | 2 | 0 | |
| z3n | 0 | 21 | 460.452 | 443.592 | 21 | 19 | 2 | 6 | 0 | 0 | |
| CVC4 | 0 | 12 | 18506.259 | 18506.559 | 12 | 10 | 2 | 15 | 14 | 0 | |
| MathSAT5n | 0 | 8 | 21744.389 | 21744.401 | 8 | 6 | 2 | 19 | 18 | 0 | |
| veriT+raSAT+Redlog | 0 | 1 | 31200.007 | 31200.01 | 1 | 1 | 0 | 26 | 26 | 0 | |
| Alt-Ergo | 0 | 0 | 31200.187 | 31200.067 | 0 | 0 | 0 | 27 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 24 | 4543.249 | 2873.555 | 24 | 24 | 0 | 3 | 1 | 0 |
| Yices2 | 0 | 23 | 10359.987 | 10360.579 | 23 | 23 | 0 | 4 | 2 | 0 |
| Yices2-fixedn | 0 | 23 | 10528.265 | 10529.069 | 23 | 23 | 0 | 4 | 2 | 0 |
| z3n | 0 | 19 | 460.072 | 443.208 | 19 | 19 | 0 | 8 | 0 | 0 |
| CVC4 | 0 | 10 | 18500.227 | 18500.527 | 10 | 10 | 0 | 17 | 14 | 0 |
| MathSAT5n | 0 | 6 | 21744.153 | 21744.165 | 6 | 6 | 0 | 21 | 18 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 28800.007 | 28800.01 | 1 | 1 | 0 | 26 | 26 | 0 |
| Alt-Ergo | 0 | 0 | 28800.187 | 28800.067 | 0 | 0 | 0 | 27 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 2 | 0.236 | 0.236 | 2 | 0 | 2 | 25 | 18 | 0 |
| 2019-Par4n | 0 | 2 | 0.012 | 0.252 | 2 | 0 | 2 | 25 | 1 | 0 |
| z3n | 0 | 2 | 0.38 | 0.383 | 2 | 0 | 2 | 25 | 0 | 0 |
| Yices2-fixedn | 0 | 2 | 0.727 | 0.727 | 2 | 0 | 2 | 25 | 2 | 0 |
| Yices2 | 0 | 2 | 0.728 | 0.728 | 2 | 0 | 2 | 25 | 2 | 0 |
| CVC4 | 0 | 2 | 6.032 | 6.032 | 2 | 0 | 2 | 25 | 14 | 0 |
| veriT+raSAT+Redlog | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 27 | 26 | 0 |
| Alt-Ergo | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 27 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 19 | 348.712 | 271.892 | 19 | 17 | 2 | 8 | 8 | 0 | |
| z3n | 0 | 17 | 302.323 | 285.448 | 17 | 15 | 2 | 10 | 6 | 0 | |
| Yices2 | 0 | 5 | 549.551 | 549.559 | 5 | 3 | 2 | 22 | 22 | 0 | |
| Yices2-fixedn | 0 | 5 | 549.664 | 549.667 | 5 | 3 | 2 | 22 | 22 | 0 | |
| MathSAT5n | 0 | 4 | 555.855 | 555.856 | 4 | 2 | 2 | 23 | 22 | 0 | |
| CVC4 | 0 | 3 | 582.051 | 582.05 | 3 | 1 | 2 | 24 | 24 | 0 | |
| veriT+raSAT+Redlog | 0 | 1 | 624.007 | 624.01 | 1 | 1 | 0 | 26 | 26 | 0 | |
| Alt-Ergo | 0 | 0 | 624.187 | 624.067 | 0 | 0 | 0 | 27 | 26 | 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.