The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFNIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 5036 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 |
Note: the division has disagreements
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3027 | 2608159.954 | 2511037.652 | 3027 | 592 | 2435 | 2009 | 2009 | 0 | |
| CVC4 | 0 | 2789 | 2655725.776 | 2729013.277 | 2789 | 571 | 2218 | 2247 | 2178 | 0 | |
| z3n | 0 | 2205 | 2256486.679 | 2258220.176 | 2205 | 510 | 1695 | 2831 | 1618 | 4 | |
| Vampire | 0 | 1742 | 4128912.762 | 3998009.61 | 1742 | 0 | 1742 | 3294 | 3294 | 0 | |
| 2018-Vampiren | 0 | 1584 | 4498882.787 | 4232338.454 | 1584 | 0 | 1584 | 3452 | 3452 | 0 | |
| Alt-Ergo | 0 | 790 | 3462659.259 | 3268625.415 | 790 | 0 | 790 | 4246 | 2518 | 124 | |
| UltimateEliminator+MathSAT | 0 | 651 | 395863.993 | 392519.848 | 651 | 508 | 143 | 4385 | 316 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3040 | 2614010.284 | 2506403.817 | 3040 | 593 | 2447 | 1996 | 1996 | 0 | |
| CVC4 | 0 | 2789 | 2725980.375 | 2728891.177 | 2789 | 571 | 2218 | 2247 | 2178 | 0 | |
| z3n | 0 | 2205 | 2258043.029 | 2258151.006 | 2205 | 510 | 1695 | 2831 | 1618 | 4 | |
| Vampire | 0 | 2153 | 4892770.572 | 3796663.411 | 2153 | 0 | 2153 | 2883 | 2883 | 0 | |
| Alt-Ergo | 0 | 833 | 3733777.999 | 3097009.735 | 833 | 0 | 833 | 4203 | 2195 | 124 | |
| UltimateEliminator+MathSAT | 0 | 651 | 396710.433 | 392097.725 | 651 | 508 | 143 | 4385 | 315 | 0 | |
| 2018-Vampiren | 1 | 2555 | 7191155.507 | 3798960.905 | 2555 | 0 | 2555 | 2481 | 2480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 593 | 37654.343 | 24443.315 | 593 | 593 | 0 | 4443 | 1996 | 0 |
| CVC4 | 0 | 571 | 44280.363 | 44481.478 | 571 | 571 | 0 | 4465 | 2178 | 0 |
| z3n | 0 | 510 | 93128.876 | 93106.596 | 510 | 510 | 0 | 4526 | 1618 | 4 |
| UltimateEliminator+MathSAT | 0 | 508 | 38306.219 | 37643.395 | 508 | 508 | 0 | 4528 | 315 | 0 |
| Alt-Ergo | 0 | 0 | 122946.193 | 119344.302 | 0 | 0 | 0 | 5036 | 2195 | 124 |
| Vampire | 0 | 0 | 740402.4 | 722362.44 | 0 | 0 | 0 | 5036 | 2883 | 0 |
| 2018-Vampiren | 1 | 41 | 1074213.89 | 714367.855 | 41 | 0 | 41 | 4995 | 2480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 2555 | 4405103.327 | 1695717.595 | 2555 | 0 | 2555 | 2481 | 2480 | 0 |
| 2019-Par4n | 0 | 2488 | 1143609.574 | 1049188.767 | 2488 | 41 | 2447 | 2548 | 1996 | 0 |
| CVC4 | 0 | 2258 | 1273347.722 | 1276069.433 | 2258 | 40 | 2218 | 2778 | 2178 | 0 |
| Vampire | 0 | 2153 | 2721966.102 | 1690761.491 | 2153 | 0 | 2153 | 2883 | 2883 | 0 |
| z3n | 0 | 1732 | 1160160.209 | 1160253.836 | 1732 | 37 | 1695 | 3304 | 1618 | 4 |
| Alt-Ergo | 0 | 833 | 2629733.797 | 2099501.74 | 833 | 0 | 833 | 4203 | 2195 | 124 |
| UltimateEliminator+MathSAT | 0 | 180 | 320946.424 | 318238.263 | 180 | 37 | 143 | 4856 | 315 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2577 | 64066.115 | 61782.582 | 2577 | 552 | 2025 | 2459 | 2459 | 0 | |
| CVC4 | 0 | 2273 | 68490.195 | 68465.246 | 2273 | 513 | 1760 | 2763 | 2756 | 0 | |
| z3n | 0 | 2096 | 66464.07 | 66396.936 | 2096 | 487 | 1609 | 2940 | 2569 | 4 | |
| Vampire | 0 | 1221 | 100752.583 | 94032.374 | 1221 | 0 | 1221 | 3815 | 3815 | 0 | |
| 2018-Vampiren | 0 | 1185 | 98863.665 | 94174.303 | 1185 | 0 | 1185 | 3851 | 3851 | 0 | |
| Alt-Ergo | 0 | 689 | 79759.32 | 75276.063 | 689 | 0 | 689 | 4347 | 2936 | 124 | |
| UltimateEliminator+MathSAT | 0 | 650 | 24380.144 | 19245.898 | 650 | 507 | 143 | 4386 | 326 | 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.