The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UF division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 2291 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | Vampire | CVC4 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 973 | 1643803.315 | 1597569.862 | 973 | 395 | 578 | 1318 | 1318 | 0 | |
| CVC4 | 0 | 963 | 1758897.314 | 1773146.516 | 963 | 338 | 625 | 1328 | 1328 | 0 | |
| 2019-CVC4n | 0 | 944 | 1910988.621 | 1935250.833 | 944 | 322 | 622 | 1347 | 1347 | 0 | |
| 2018-Vampiren | 0 | 840 | 1813228.808 | 1759401.079 | 840 | 378 | 462 | 1451 | 1451 | 0 | |
| veriT | 0 | 588 | 2077365.21 | 2077660.348 | 588 | 0 | 588 | 1703 | 1677 | 25 | |
| veriT+viten | 0 | 548 | 2086625.231 | 2086813.985 | 548 | 0 | 548 | 1743 | 1496 | 235 | |
| Alt-Ergo | 0 | 509 | 2080431.516 | 2062072.741 | 509 | 0 | 509 | 1782 | 1674 | 38 | |
| z3n | 0 | 413 | 1726958.333 | 1727292.972 | 413 | 63 | 350 | 1878 | 1108 | 40 | |
| SMTInterpol-fixedn | 0 | 105 | 2612731.006 | 2612205.548 | 105 | 25 | 80 | 2186 | 2174 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 8276.599 | 5505.553 | 0 | 0 | 0 | 2291 | 0 | 0 | |
| SMTInterpol | 1 | 104 | 2612727.736 | 2612212.162 | 104 | 25 | 79 | 2187 | 2174 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1008 | 1702696.105 | 1580071.11 | 1008 | 399 | 609 | 1283 | 1283 | 0 | |
| 2018-Vampiren | 0 | 963 | 2340432.818 | 1683107.238 | 963 | 380 | 583 | 1328 | 1328 | 0 | |
| CVC4 | 0 | 963 | 1769821.134 | 1773088.026 | 963 | 338 | 625 | 1328 | 1328 | 0 | |
| 2019-CVC4n | 0 | 946 | 1930178.236 | 1935088.213 | 946 | 324 | 622 | 1345 | 1345 | 0 | |
| veriT | 0 | 588 | 2077587.71 | 2077592.118 | 588 | 0 | 588 | 1703 | 1677 | 25 | |
| veriT+viten | 0 | 548 | 2086772.061 | 2086757.405 | 548 | 0 | 548 | 1743 | 1496 | 235 | |
| Alt-Ergo | 0 | 531 | 2162172.196 | 2048035.975 | 531 | 0 | 531 | 1760 | 1650 | 38 | |
| z3n | 0 | 413 | 1727169.923 | 1727245.922 | 413 | 63 | 350 | 1878 | 1108 | 40 | |
| SMTInterpol-fixedn | 0 | 105 | 2648041.906 | 2604284.502 | 105 | 25 | 80 | 2186 | 2151 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 8276.599 | 5505.553 | 0 | 0 | 0 | 2291 | 0 | 0 | |
| SMTInterpol | 1 | 104 | 2644135.176 | 2604052.602 | 104 | 25 | 79 | 2187 | 2152 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 399 | 48599.724 | 20509.544 | 399 | 399 | 0 | 1892 | 1283 | 0 |
| 2018-Vampiren | 0 | 380 | 58114.677 | 38901.72 | 380 | 380 | 0 | 1911 | 1328 | 0 |
| CVC4 | 0 | 338 | 236920.444 | 239970.226 | 338 | 338 | 0 | 1953 | 1328 | 0 |
| 2019-CVC4n | 0 | 324 | 383250.437 | 387934.826 | 324 | 324 | 0 | 1967 | 1345 | 0 |
| z3n | 0 | 63 | 312126.677 | 312138.952 | 63 | 63 | 0 | 2228 | 1108 | 40 |
| SMTInterpol | 0 | 25 | 449505.582 | 445652.658 | 25 | 25 | 0 | 2266 | 2152 | 0 |
| SMTInterpol-fixedn | 0 | 25 | 449545.292 | 445696.926 | 25 | 25 | 0 | 2266 | 2151 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1438.868 | 974.197 | 0 | 0 | 0 | 2291 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 434927.964 | 416704.774 | 0 | 0 | 0 | 2291 | 1650 | 38 |
| veriT | 0 | 0 | 489600.0 | 489600.0 | 0 | 0 | 0 | 2291 | 1677 | 25 |
| veriT+viten | 0 | 0 | 489600.0 | 489600.0 | 0 | 0 | 0 | 2291 | 1496 | 235 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 625 | 90500.69 | 90717.8 | 625 | 0 | 625 | 1666 | 1328 | 0 |
| 2019-CVC4n | 0 | 622 | 104527.798 | 104753.386 | 622 | 0 | 622 | 1669 | 1345 | 0 |
| Vampire | 0 | 609 | 204495.741 | 117177.895 | 609 | 0 | 609 | 1682 | 1283 | 0 |
| veriT | 0 | 588 | 146160.29 | 146164.41 | 588 | 0 | 588 | 1703 | 1677 | 25 |
| 2018-Vampiren | 0 | 583 | 476247.331 | 203368.288 | 583 | 0 | 583 | 1708 | 1328 | 0 |
| veriT+viten | 0 | 548 | 162687.138 | 162671.795 | 548 | 0 | 548 | 1743 | 1496 | 235 |
| Alt-Ergo | 0 | 531 | 262274.905 | 199806.169 | 531 | 0 | 531 | 1760 | 1650 | 38 |
| z3n | 0 | 350 | 311738.15 | 311748.339 | 350 | 0 | 350 | 1941 | 1108 | 40 |
| SMTInterpol-fixedn | 0 | 80 | 729656.704 | 720418.588 | 80 | 0 | 80 | 2211 | 2151 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 2477.378 | 1636.732 | 0 | 0 | 0 | 2291 | 0 | 0 |
| SMTInterpol | 1 | 79 | 727004.724 | 720615.347 | 79 | 0 | 79 | 2212 | 2152 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 793 | 41101.055 | 37348.417 | 793 | 323 | 470 | 1498 | 1498 | 0 | |
| 2018-Vampiren | 0 | 708 | 42853.115 | 39306.871 | 708 | 338 | 370 | 1583 | 1583 | 0 | |
| veriT+viten | 0 | 534 | 43041.1 | 43025.434 | 534 | 0 | 534 | 1757 | 1521 | 235 | |
| 2019-CVC4n | 0 | 516 | 42998.979 | 42976.38 | 516 | 27 | 489 | 1775 | 1775 | 0 | |
| CVC4 | 0 | 515 | 42996.77 | 42994.015 | 515 | 27 | 488 | 1776 | 1776 | 0 | |
| veriT | 0 | 467 | 44252.743 | 44252.679 | 467 | 0 | 467 | 1824 | 1799 | 25 | |
| Alt-Ergo | 0 | 466 | 46210.435 | 43425.886 | 466 | 0 | 466 | 1825 | 1728 | 38 | |
| z3n | 0 | 380 | 46234.752 | 46226.228 | 380 | 59 | 321 | 1911 | 1871 | 40 | |
| SMTInterpol-fixedn | 0 | 99 | 52664.167 | 52501.651 | 99 | 25 | 74 | 2192 | 2182 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 8276.599 | 5505.553 | 0 | 0 | 0 | 2291 | 0 | 0 | |
| SMTInterpol | 1 | 98 | 52674.453 | 52501.126 | 98 | 25 | 73 | 2193 | 2182 | 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.