The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the LRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 802 Time Limit: 1200 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 755 | 76904.603 | 66708.316 | 755 | 310 | 445 | 47 | 47 | 0 | |
| z3n | 0 | 744 | 103284.173 | 103275.467 | 744 | 305 | 439 | 58 | 58 | 0 | |
| 2019-Z3n | 0 | 742 | 103542.378 | 103546.408 | 742 | 305 | 437 | 60 | 60 | 0 | |
| CVC4 | 0 | 653 | 201426.837 | 202297.426 | 653 | 269 | 384 | 149 | 149 | 0 | |
| UltimateEliminator+MathSAT | 0 | 504 | 370033.47 | 368155.787 | 504 | 201 | 303 | 298 | 297 | 0 | |
| Vampire | 0 | 222 | 715390.128 | 702806.272 | 222 | 0 | 222 | 580 | 580 | 0 | |
| SMTInterpol | 0 | 132 | 19655.618 | 18391.48 | 132 | 1 | 131 | 670 | 14 | 0 | |
| SMTInterpol-fixedn | 0 | 132 | 19669.496 | 18408.514 | 132 | 1 | 131 | 670 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 760 | 79786.403 | 65156.776 | 760 | 312 | 448 | 42 | 42 | 0 | |
| z3n | 0 | 744 | 103287.313 | 103273.567 | 744 | 305 | 439 | 58 | 58 | 0 | |
| 2019-Z3n | 0 | 742 | 103547.878 | 103544.068 | 742 | 305 | 437 | 60 | 60 | 0 | |
| CVC4 | 0 | 653 | 201706.907 | 202291.346 | 653 | 269 | 384 | 149 | 149 | 0 | |
| UltimateEliminator+MathSAT | 0 | 504 | 370033.47 | 368155.787 | 504 | 201 | 303 | 298 | 297 | 0 | |
| Vampire | 0 | 237 | 739115.338 | 693847.327 | 237 | 0 | 237 | 565 | 565 | 0 | |
| SMTInterpol | 0 | 132 | 19655.618 | 18391.48 | 132 | 1 | 131 | 670 | 14 | 0 | |
| SMTInterpol-fixedn | 0 | 132 | 19669.496 | 18408.514 | 132 | 1 | 131 | 670 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 312 | 20829.361 | 15243.897 | 312 | 312 | 0 | 490 | 42 | 0 |
| 2019-Z3n | 0 | 305 | 24943.113 | 24944.059 | 305 | 305 | 0 | 497 | 60 | 0 |
| z3n | 0 | 305 | 25132.246 | 25125.705 | 305 | 305 | 0 | 497 | 58 | 0 |
| CVC4 | 0 | 269 | 70934.037 | 71271.283 | 269 | 269 | 0 | 533 | 149 | 0 |
| UltimateEliminator+MathSAT | 0 | 201 | 144077.879 | 143398.938 | 201 | 201 | 0 | 601 | 297 | 0 |
| SMTInterpol | 0 | 1 | 14949.868 | 14359.058 | 1 | 1 | 0 | 801 | 14 | 0 |
| SMTInterpol-fixedn | 0 | 1 | 14992.736 | 14377.238 | 1 | 1 | 0 | 801 | 14 | 0 |
| Vampire | 0 | 0 | 391200.32 | 383975.89 | 0 | 0 | 0 | 802 | 565 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 448 | 44557.041 | 35512.879 | 448 | 0 | 448 | 354 | 42 | 0 |
| z3n | 0 | 439 | 63755.067 | 63747.863 | 439 | 0 | 439 | 363 | 58 | 0 |
| 2019-Z3n | 0 | 437 | 64204.765 | 64200.01 | 437 | 0 | 437 | 365 | 60 | 0 |
| CVC4 | 0 | 384 | 116372.87 | 116620.063 | 384 | 0 | 384 | 418 | 149 | 0 |
| UltimateEliminator+MathSAT | 0 | 303 | 211555.591 | 210356.849 | 303 | 0 | 303 | 499 | 297 | 0 |
| Vampire | 0 | 237 | 333515.018 | 295471.437 | 237 | 0 | 237 | 565 | 565 | 0 |
| SMTInterpol-fixedn | 0 | 131 | 4637.41 | 4018.25 | 131 | 0 | 131 | 671 | 14 | 0 |
| SMTInterpol | 0 | 131 | 4670.701 | 4019.3 | 131 | 0 | 131 | 671 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 694 | 3921.923 | 3298.561 | 694 | 289 | 405 | 108 | 108 | 0 | |
| z3n | 0 | 642 | 5114.393 | 5097.564 | 642 | 279 | 363 | 160 | 160 | 0 | |
| 2019-Z3n | 0 | 641 | 5209.609 | 5202.519 | 641 | 279 | 362 | 161 | 161 | 0 | |
| CVC4 | 0 | 593 | 5222.645 | 5222.518 | 593 | 244 | 349 | 209 | 209 | 0 | |
| UltimateEliminator+MathSAT | 0 | 455 | 10851.2 | 9782.643 | 455 | 191 | 264 | 347 | 346 | 0 | |
| Vampire | 0 | 144 | 16420.483 | 15980.628 | 144 | 0 | 144 | 658 | 658 | 0 | |
| SMTInterpol-fixedn | 0 | 132 | 2379.787 | 1297.818 | 132 | 1 | 131 | 670 | 23 | 0 | |
| SMTInterpol | 0 | 132 | 2371.876 | 1299.02 | 132 | 1 | 131 | 670 | 23 | 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.