The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearIntArith division in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 4456 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 4188 | 406670.018 | 346322.523 | 4188 | 2426 | 1762 | 268 | 0 | 268 | 0 |
| cvc5 | 0 | 3893 | 1060522.717 | 1060271.806 | 3893 | 2164 | 1729 | 563 | 0 | 560 | 0 |
| cvc5 - fixedn | 0 | 3892 | 1061093.111 | 1060928.465 | 3892 | 2163 | 1729 | 564 | 0 | 561 | 0 |
| z3n | 0 | 3847 | 948799.919 | 948953.441 | 3847 | 2251 | 1596 | 609 | 0 | 609 | 0 |
| MathSAT5n | 0 | 3801 | 1096241.732 | 1096596.514 | 3801 | 2139 | 1662 | 655 | 0 | 655 | 0 |
| Yices2 | 0 | 3786 | 885674.485 | 885684.729 | 3786 | 2125 | 1661 | 670 | 0 | 670 | 0 |
| SMTInterpol | 0 | 3192 | 1778887.663 | 1734184.464 | 3192 | 1871 | 1321 | 1264 | 0 | 1264 | 0 |
| OpenSMT - fixedn | 0 | 3170 | 1701147.363 | 1813258.154 | 3170 | 1675 | 1495 | 1279 | 7 | 764 | 0 |
| veriT | 0 | 2081 | 2478556.263 | 2478659.321 | 2081 | 1297 | 784 | 2375 | 0 | 1926 | 0 |
| YicesLS | 0 | 1009 | 187459.02 | 187522.635 | 1009 | 625 | 384 | 129 | 3318 | 63 | 0 |
| OpenSMT | 8 | 3167 | 1693487.277 | 1807971.941 | 3167 | 1679 | 1488 | 1282 | 7 | 782 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 4261 | 495273.288 | 306830.628 | 4261 | 2467 | 1794 | 195 | 0 | 195 | 0 |
| cvc5 | 0 | 3893 | 1060600.347 | 1060250.246 | 3893 | 2164 | 1729 | 563 | 0 | 560 | 0 |
| cvc5 - fixedn | 0 | 3892 | 1061170.031 | 1060906.115 | 3892 | 2163 | 1729 | 564 | 0 | 561 | 0 |
| z3n | 0 | 3847 | 949089.789 | 948928.201 | 3847 | 2251 | 1596 | 609 | 0 | 609 | 0 |
| MathSAT5n | 0 | 3801 | 1096655.642 | 1096568.664 | 3801 | 2139 | 1662 | 655 | 0 | 655 | 0 |
| Yices2 | 0 | 3786 | 885718.925 | 885667.089 | 3786 | 2125 | 1661 | 670 | 0 | 670 | 0 |
| SMTInterpol | 0 | 3193 | 1778897.593 | 1734048.914 | 3193 | 1872 | 1321 | 1263 | 0 | 1263 | 0 |
| OpenSMT - fixedn | 0 | 3170 | 1727183.023 | 1813228.864 | 3170 | 1675 | 1495 | 1279 | 7 | 764 | 0 |
| veriT | 0 | 2081 | 2478696.093 | 2478597.841 | 2081 | 1297 | 784 | 2375 | 0 | 1926 | 0 |
| YicesLS | 0 | 1009 | 187477.24 | 187520.935 | 1009 | 625 | 384 | 129 | 3318 | 119 | 0 |
| OpenSMT | 8 | 3167 | 1725806.015 | 1807946.591 | 3167 | 1679 | 1488 | 1282 | 7 | 783 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2467 | 262545.759 | 153080.982 | 2467 | 2467 | 0 | 91 | 1898 | 195 | 0 |
| z3n | 0 | 2251 | 507567.266 | 507580.987 | 2251 | 2251 | 0 | 307 | 1898 | 609 | 0 |
| cvc5 | 0 | 2164 | 675832.559 | 675680.126 | 2164 | 2164 | 0 | 394 | 1898 | 560 | 0 |
| cvc5 - fixedn | 0 | 2163 | 676438.455 | 676209.605 | 2163 | 2163 | 0 | 395 | 1898 | 561 | 0 |
| MathSAT5n | 0 | 2139 | 652618.686 | 652530.579 | 2139 | 2139 | 0 | 419 | 1898 | 655 | 0 |
| Yices2 | 0 | 2125 | 582427.159 | 582385.458 | 2125 | 2125 | 0 | 433 | 1898 | 670 | 0 |
| SMTInterpol | 0 | 1872 | 1010578.416 | 983761.716 | 1872 | 1872 | 0 | 686 | 1898 | 1263 | 0 |
| OpenSMT - fixedn | 0 | 1675 | 1176586.902 | 1255724.492 | 1675 | 1675 | 0 | 882 | 1899 | 764 | 0 |
| veriT | 0 | 1297 | 1205498.374 | 1205395.459 | 1297 | 1297 | 0 | 1261 | 1898 | 1926 | 0 |
| YicesLS | 0 | 625 | 83020.431 | 83061.32 | 625 | 625 | 0 | 52 | 3779 | 119 | 0 |
| OpenSMT | 8 | 1679 | 1175745.067 | 1251160.069 | 1679 | 1679 | 0 | 878 | 1899 | 783 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1794 | 183527.53 | 104549.647 | 1794 | 0 | 1794 | 63 | 2599 | 195 | 0 |
| cvc5 | 0 | 1729 | 335567.788 | 335370.12 | 1729 | 0 | 1729 | 128 | 2599 | 560 | 0 |
| cvc5 - fixedn | 0 | 1729 | 335531.576 | 335496.51 | 1729 | 0 | 1729 | 128 | 2599 | 561 | 0 |
| MathSAT5n | 0 | 1662 | 394836.956 | 394838.085 | 1662 | 0 | 1662 | 195 | 2599 | 655 | 0 |
| Yices2 | 0 | 1661 | 254091.766 | 254081.631 | 1661 | 0 | 1661 | 196 | 2599 | 670 | 0 |
| z3n | 0 | 1596 | 392322.524 | 392147.215 | 1596 | 0 | 1596 | 261 | 2599 | 609 | 0 |
| OpenSMT - fixedn | 0 | 1495 | 501396.122 | 508304.373 | 1495 | 0 | 1495 | 356 | 2605 | 764 | 0 |
| OpenSMT | 0 | 1488 | 500860.947 | 507586.522 | 1488 | 0 | 1488 | 363 | 2605 | 783 | 0 |
| SMTInterpol | 0 | 1321 | 719119.177 | 701087.198 | 1321 | 0 | 1321 | 536 | 2599 | 1263 | 0 |
| veriT | 0 | 784 | 1223997.72 | 1224002.382 | 784 | 0 | 784 | 1073 | 2599 | 1926 | 0 |
| YicesLS | 0 | 384 | 68457.479 | 68459.614 | 384 | 0 | 384 | 47 | 4025 | 119 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3985 | 22581.403 | 15156.602 | 3985 | 2298 | 1687 | 471 | 0 | 471 | 0 |
| Yices2 | 0 | 3490 | 27771.008 | 27713.003 | 3490 | 1905 | 1585 | 966 | 0 | 966 | 0 |
| z3n | 0 | 2906 | 46120.658 | 45998.626 | 2906 | 1659 | 1247 | 1550 | 0 | 1550 | 0 |
| MathSAT5n | 0 | 2543 | 52383.572 | 52302.746 | 2543 | 1469 | 1074 | 1913 | 0 | 1913 | 0 |
| cvc5 | 0 | 2199 | 60093.148 | 59971.656 | 2199 | 1245 | 954 | 2257 | 0 | 2257 | 0 |
| cvc5 - fixedn | 0 | 2197 | 60121.604 | 59992.473 | 2197 | 1245 | 952 | 2259 | 0 | 2259 | 0 |
| SMTInterpol | 0 | 1962 | 82234.846 | 69324.663 | 1962 | 1075 | 887 | 2494 | 0 | 2494 | 0 |
| OpenSMT - fixedn | 0 | 1850 | 71258.067 | 71146.334 | 1850 | 876 | 974 | 2599 | 7 | 2595 | 0 |
| veriT | 0 | 1560 | 64990.242 | 64940.719 | 1560 | 943 | 617 | 2896 | 0 | 2529 | 0 |
| YicesLS | 0 | 833 | 8856.22 | 8889.543 | 833 | 526 | 307 | 305 | 3318 | 305 | 0 |
| OpenSMT | 8 | 1847 | 71113.902 | 71008.439 | 1847 | 880 | 967 | 2602 | 7 | 2590 | 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.