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 2019-07-23 17:56:09 +0000
Benchmarks: 1003 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 945 | 223885.451 | 223926.711 | 945 | 368 | 577 | 58 | 58 | 0 | |
| Par4 | 0 | 941 | 191786.877 | 170445.269 | 941 | 371 | 570 | 62 | 62 | 0 | |
| 2018-Z3n | 0 | 931 | 263064.491 | 263064.501 | 931 | 366 | 565 | 72 | 72 | 0 | |
| CVC4 | 0 | 815 | 527431.59 | 532098.4 | 815 | 312 | 503 | 188 | 188 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 654 | 863725.43 | 859053.7 | 654 | 222 | 432 | 349 | 348 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 650 | 871513.733 | 868354.119 | 650 | 222 | 428 | 353 | 351 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 366 | 129268.51 | 132382.002 | 366 | 147 | 219 | 637 | 54 | 0 | |
| Vampire | 0 | 223 | 1936562.617 | 1888283.873 | 223 | 0 | 223 | 780 | 780 | 0 | |
| SMTInterpol | 0 | 152 | 66069.515 | 63342.322 | 152 | 3 | 149 | 851 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 959 | 208579.777 | 157110.129 | 959 | 374 | 585 | 44 | 44 | 0 | |
| Z3n | 0 | 945 | 223907.291 | 223924.401 | 945 | 368 | 577 | 58 | 58 | 0 | |
| 2018-Z3n | 0 | 931 | 263071.751 | 263062.481 | 931 | 366 | 565 | 72 | 72 | 0 | |
| CVC4 | 0 | 815 | 530547.78 | 532089.07 | 815 | 312 | 503 | 188 | 188 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 654 | 863725.43 | 859053.7 | 654 | 222 | 432 | 349 | 348 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 650 | 871513.733 | 868354.119 | 650 | 222 | 428 | 353 | 351 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 366 | 134056.58 | 132381.402 | 366 | 147 | 219 | 637 | 54 | 0 | |
| Vampire | 0 | 228 | 1996128.137 | 1882520.796 | 228 | 0 | 228 | 775 | 775 | 0 | |
| SMTInterpol | 0 | 152 | 66069.515 | 63342.322 | 152 | 3 | 149 | 851 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 374 | 28756.231 | 16844.534 | 374 | 374 | 0 | 629 | 44 | 0 |
| Z3n | 0 | 368 | 34444.35 | 34445.772 | 368 | 368 | 0 | 635 | 58 | 0 |
| 2018-Z3n | 0 | 366 | 41246.388 | 41247.195 | 366 | 366 | 0 | 637 | 72 | 0 |
| CVC4 | 0 | 312 | 185842.04 | 186748.691 | 312 | 312 | 0 | 691 | 188 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 222 | 374836.13 | 373711.271 | 222 | 222 | 0 | 781 | 348 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 222 | 375949.478 | 374764.52 | 222 | 222 | 0 | 781 | 351 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 147 | 102614.377 | 101963.856 | 147 | 147 | 0 | 856 | 54 | 0 |
| SMTInterpol | 0 | 3 | 50151.281 | 48972.237 | 3 | 3 | 0 | 1000 | 20 | 0 |
| Vampire | 0 | 0 | 931201.2 | 901778.12 | 0 | 0 | 0 | 1003 | 775 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 585 | 110223.546 | 70665.596 | 585 | 0 | 585 | 418 | 44 | 0 |
| Z3n | 0 | 577 | 119862.941 | 119878.629 | 577 | 0 | 577 | 426 | 58 | 0 |
| 2018-Z3n | 0 | 565 | 152225.363 | 152215.286 | 565 | 0 | 565 | 438 | 72 | 0 |
| CVC4 | 0 | 503 | 275105.74 | 275740.379 | 503 | 0 | 503 | 500 | 188 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 432 | 419289.3 | 415742.428 | 432 | 0 | 432 | 571 | 348 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 428 | 425964.255 | 423989.599 | 428 | 0 | 428 | 575 | 351 | 0 |
| Vampire | 0 | 228 | 995326.937 | 911142.676 | 228 | 0 | 228 | 775 | 775 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 219 | 28859.549 | 27915.927 | 219 | 0 | 219 | 784 | 54 | 0 |
| SMTInterpol | 0 | 149 | 14950.363 | 13509.312 | 149 | 0 | 149 | 854 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 851 | 5341.94 | 4546.927 | 851 | 337 | 514 | 152 | 152 | 0 | |
| Z3n | 0 | 783 | 6882.257 | 6883.06 | 783 | 332 | 451 | 220 | 220 | 0 | |
| 2018-Z3n | 0 | 749 | 7934.34 | 7920.521 | 749 | 319 | 430 | 254 | 254 | 0 | |
| CVC4 | 0 | 704 | 7436.468 | 7437.749 | 704 | 272 | 432 | 299 | 299 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 577 | 14632.563 | 12400.84 | 577 | 204 | 373 | 426 | 426 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 576 | 13832.946 | 12379.637 | 576 | 204 | 372 | 427 | 427 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 365 | 5494.646 | 3890.211 | 365 | 146 | 219 | 638 | 60 | 0 | |
| SMTInterpol | 0 | 148 | 4987.587 | 3137.887 | 148 | 3 | 145 | 855 | 79 | 0 | |
| Vampire | 0 | 141 | 21876.9 | 21012.096 | 141 | 0 | 141 | 862 | 862 | 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.