The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFNIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 300 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 285 | 2710.693 | 2711.335 | 285 | 175 | 110 | 15 | 1 | 0 | |
| MathSAT-default | 0 | 270 | 76062.695 | 76068.55 | 270 | 160 | 110 | 30 | 30 | 0 | |
| 2018-Yicesn | 0 | 268 | 50701.869 | 50708.43 | 268 | 170 | 98 | 32 | 21 | 0 | |
| Yices 2.6.2 | 0 | 268 | 50762.306 | 50770.931 | 268 | 170 | 98 | 32 | 21 | 0 | |
| Z3n | 0 | 264 | 59509.047 | 59513.202 | 264 | 154 | 110 | 36 | 22 | 0 | |
| MathSAT-na-ext | 0 | 259 | 100270.792 | 100279.181 | 259 | 149 | 110 | 41 | 41 | 0 | |
| Alt-Ergo | 0 | 71 | 50.84 | 21.119 | 71 | 0 | 71 | 229 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 285 | 2711.193 | 2711.235 | 285 | 175 | 110 | 15 | 1 | 0 | |
| MathSAT-default | 0 | 270 | 76067.355 | 76067.46 | 270 | 160 | 110 | 30 | 30 | 0 | |
| 2018-Yicesn | 0 | 268 | 50707.199 | 50707.63 | 268 | 170 | 98 | 32 | 21 | 0 | |
| Yices 2.6.2 | 0 | 268 | 50769.736 | 50770.291 | 268 | 170 | 98 | 32 | 21 | 0 | |
| Z3n | 0 | 264 | 59511.797 | 59512.362 | 264 | 154 | 110 | 36 | 22 | 0 | |
| MathSAT-na-ext | 0 | 259 | 100277.352 | 100277.661 | 259 | 149 | 110 | 41 | 41 | 0 | |
| Alt-Ergo | 0 | 71 | 50.84 | 21.119 | 71 | 0 | 71 | 229 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 175 | 300.4 | 300.465 | 175 | 175 | 0 | 125 | 1 | 0 |
| 2018-Yicesn | 0 | 170 | 2705.806 | 2706.008 | 170 | 170 | 0 | 130 | 21 | 0 |
| Yices 2.6.2 | 0 | 170 | 2768.254 | 2768.551 | 170 | 170 | 0 | 130 | 21 | 0 |
| MathSAT-default | 0 | 160 | 49646.011 | 49646.106 | 160 | 160 | 0 | 140 | 30 | 0 |
| Z3n | 0 | 154 | 44461.549 | 44461.939 | 154 | 154 | 0 | 146 | 22 | 0 |
| MathSAT-na-ext | 0 | 149 | 73847.765 | 73848.062 | 149 | 149 | 0 | 151 | 41 | 0 |
| Alt-Ergo | 0 | 0 | 38.885 | 14.976 | 0 | 0 | 0 | 300 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 110 | 5.337 | 5.314 | 110 | 0 | 110 | 190 | 1 | 0 |
| Z3n | 0 | 110 | 7724.986 | 7725.136 | 110 | 0 | 110 | 190 | 22 | 0 |
| MathSAT-default | 0 | 110 | 16821.344 | 16821.355 | 110 | 0 | 110 | 190 | 30 | 0 |
| MathSAT-na-ext | 0 | 110 | 16829.587 | 16829.599 | 110 | 0 | 110 | 190 | 41 | 0 |
| 2018-Yicesn | 0 | 98 | 38401.393 | 38401.622 | 98 | 0 | 98 | 202 | 21 | 0 |
| Yices 2.6.2 | 0 | 98 | 38401.482 | 38401.74 | 98 | 0 | 98 | 202 | 21 | 0 |
| Alt-Ergo | 0 | 71 | 11.145 | 5.828 | 71 | 0 | 71 | 229 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 283 | 120.66 | 120.628 | 283 | 173 | 110 | 17 | 3 | 0 | |
| 2018-Yicesn | 0 | 266 | 568.423 | 568.848 | 266 | 168 | 98 | 34 | 23 | 0 | |
| Yices 2.6.2 | 0 | 266 | 571.218 | 571.732 | 266 | 168 | 98 | 34 | 23 | 0 | |
| MathSAT-default | 0 | 266 | 990.553 | 990.576 | 266 | 156 | 110 | 34 | 34 | 0 | |
| Z3n | 0 | 254 | 1190.89 | 1190.904 | 254 | 146 | 108 | 46 | 45 | 0 | |
| MathSAT-na-ext | 0 | 252 | 1266.419 | 1266.442 | 252 | 142 | 110 | 48 | 48 | 0 | |
| Alt-Ergo | 0 | 71 | 50.84 | 21.119 | 71 | 0 | 71 | 229 | 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.