The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFNIRA 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) |
|---|---|---|---|---|
| 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 | 62 | 577498.135 | 574451.769 | 62 | 3 | 59 | 238 | 232 | 6 | |
| CVC4 | 0 | 58 | 562394.729 | 585027.728 | 58 | 1 | 57 | 242 | 239 | 0 | |
| 2018-CVC4n | 0 | 57 | 576360.664 | 580819.896 | 57 | 1 | 56 | 243 | 240 | 0 | |
| Vampire | 0 | 51 | 605970.742 | 599715.405 | 51 | 0 | 51 | 249 | 249 | 0 | |
| Z3n | 0 | 40 | 279014.839 | 284074.051 | 40 | 3 | 37 | 260 | 47 | 3 | |
| Alt-Ergo | 0 | 37 | 633510.542 | 629989.807 | 37 | 0 | 37 | 263 | 261 | 1 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 952.187 | 799.004 | 0 | 0 | 0 | 300 | 0 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 3426.439 | 3923.235 | 0 | 0 | 0 | 300 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 63 | 579231.445 | 574140.829 | 63 | 3 | 60 | 237 | 231 | 6 | |
| CVC4 | 0 | 58 | 584791.509 | 585015.518 | 58 | 1 | 57 | 242 | 239 | 0 | |
| 2018-CVC4n | 0 | 57 | 580753.004 | 580809.846 | 57 | 1 | 56 | 243 | 240 | 0 | |
| Vampire | 0 | 57 | 611447.172 | 590308.435 | 57 | 0 | 57 | 243 | 243 | 0 | |
| Z3n | 0 | 40 | 279505.649 | 284071.741 | 40 | 3 | 37 | 260 | 47 | 3 | |
| Alt-Ergo | 0 | 37 | 647912.142 | 629787.797 | 37 | 0 | 37 | 263 | 261 | 1 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 952.187 | 799.004 | 0 | 0 | 0 | 300 | 0 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 3426.439 | 3923.235 | 0 | 0 | 0 | 300 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3 | 0.018 | 0.068 | 3 | 3 | 0 | 297 | 231 | 6 |
| Z3n | 0 | 3 | 0.113 | 0.113 | 3 | 3 | 0 | 297 | 47 | 3 |
| 2018-CVC4n | 0 | 1 | 2884.598 | 2906.816 | 1 | 1 | 0 | 299 | 240 | 0 |
| CVC4 | 0 | 1 | 3366.157 | 3404.964 | 1 | 1 | 0 | 299 | 239 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 9.379 | 6.885 | 0 | 0 | 0 | 300 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 10.192 | 7.098 | 0 | 0 | 0 | 300 | 1 | 0 |
| Alt-Ergo | 0 | 0 | 4800.139 | 4800.052 | 0 | 0 | 0 | 300 | 261 | 1 |
| Vampire | 0 | 0 | 7200.0 | 7200.0 | 0 | 0 | 0 | 300 | 243 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 60 | 24831.427 | 19740.76 | 60 | 0 | 60 | 240 | 231 | 6 |
| Vampire | 0 | 57 | 49847.172 | 28708.435 | 57 | 0 | 57 | 243 | 243 | 0 |
| CVC4 | 0 | 57 | 30381.755 | 30560.979 | 57 | 0 | 57 | 243 | 239 | 0 |
| 2018-CVC4n | 0 | 56 | 27515.244 | 27576.474 | 56 | 0 | 56 | 244 | 240 | 0 |
| Z3n | 0 | 37 | 28515.698 | 29182.898 | 37 | 0 | 37 | 263 | 47 | 3 |
| Alt-Ergo | 0 | 37 | 74310.403 | 70789.755 | 37 | 0 | 37 | 263 | 261 | 1 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 209.835 | 151.504 | 0 | 0 | 0 | 300 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 224.418 | 159.201 | 0 | 0 | 0 | 300 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 44 | 6241.575 | 6196.173 | 44 | 3 | 41 | 256 | 250 | 6 | |
| Vampire | 0 | 41 | 7238.702 | 6479.314 | 41 | 0 | 41 | 259 | 259 | 0 | |
| Z3n | 0 | 37 | 5929.752 | 5929.755 | 37 | 3 | 34 | 263 | 243 | 3 | |
| 2018-CVC4n | 0 | 34 | 6418.371 | 6418.364 | 34 | 0 | 34 | 266 | 265 | 0 | |
| Alt-Ergo | 0 | 32 | 6658.202 | 6474.384 | 32 | 0 | 32 | 268 | 266 | 1 | |
| CVC4 | 0 | 31 | 6449.333 | 6449.321 | 31 | 0 | 31 | 269 | 268 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 972.85 | 705.193 | 0 | 0 | 0 | 300 | 1 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 1090.85 | 782.862 | 0 | 0 | 0 | 300 | 3 | 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.