The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_FP division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 248 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 | COLIBRI |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 202 | 129791.892 | 116901.241 | 202 | 105 | 97 | 46 | 46 | 0 | |
| COLIBRI | 0 | 196 | 128008.372 | 128018.173 | 196 | 99 | 97 | 52 | 52 | 0 | |
| CVC4 | 0 | 180 | 196158.121 | 196169.985 | 180 | 100 | 80 | 68 | 68 | 0 | |
| 2018-COLIBRIn | 0 | 175 | 167501.338 | 167509.634 | 175 | 87 | 88 | 73 | 65 | 0 | |
| Z3n | 0 | 160 | 282048.777 | 282089.207 | 160 | 83 | 77 | 88 | 88 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 209 | 146680.232 | 111333.589 | 209 | 109 | 100 | 39 | 39 | 0 | |
| COLIBRI | 0 | 196 | 128015.342 | 128016.203 | 196 | 99 | 97 | 52 | 52 | 0 | |
| CVC4 | 0 | 180 | 196176.551 | 196166.875 | 180 | 100 | 80 | 68 | 68 | 0 | |
| 2018-COLIBRIn | 0 | 175 | 167509.698 | 167506.954 | 175 | 87 | 88 | 73 | 65 | 0 | |
| Z3n | 0 | 160 | 282074.257 | 282084.977 | 160 | 83 | 77 | 88 | 88 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 109 | 55783.662 | 36213.378 | 109 | 109 | 0 | 139 | 39 | 0 |
| CVC4 | 0 | 100 | 62274.455 | 62262.227 | 100 | 100 | 0 | 148 | 68 | 0 |
| COLIBRI | 0 | 99 | 51216.296 | 51216.788 | 99 | 99 | 0 | 149 | 52 | 0 |
| 2018-COLIBRIn | 0 | 87 | 67402.009 | 67403.162 | 87 | 87 | 0 | 161 | 65 | 0 |
| Z3n | 0 | 83 | 124323.789 | 124330.006 | 83 | 83 | 0 | 165 | 88 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 100 | 50096.57 | 34320.211 | 100 | 0 | 100 | 148 | 39 | 0 |
| COLIBRI | 0 | 97 | 35999.046 | 35999.415 | 97 | 0 | 97 | 151 | 52 | 0 |
| 2018-COLIBRIn | 0 | 88 | 59307.689 | 59303.792 | 88 | 0 | 88 | 160 | 65 | 0 |
| CVC4 | 0 | 80 | 93102.096 | 93104.648 | 80 | 0 | 80 | 168 | 68 | 0 |
| Z3n | 0 | 77 | 116950.468 | 116954.971 | 77 | 0 | 77 | 171 | 88 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 179 | 2131.288 | 2132.037 | 179 | 93 | 86 | 69 | 69 | 0 | |
| Par4 | 0 | 169 | 3177.462 | 2356.894 | 169 | 87 | 82 | 79 | 79 | 0 | |
| 2018-COLIBRIn | 0 | 154 | 2626.921 | 2623.414 | 154 | 80 | 74 | 94 | 88 | 0 | |
| CVC4 | 0 | 113 | 3913.072 | 3898.922 | 113 | 64 | 49 | 135 | 135 | 0 | |
| Z3n | 0 | 43 | 5217.086 | 5217.113 | 43 | 24 | 19 | 205 | 205 | 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.