The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_LinearIntArith (QF_LIA, QF_LIRA, QF_IDL) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 3349 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | SMTInterpol | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3206 | 413634.323 | 364384.2 | 3206 | 1868 | 1338 | 143 | 143 | 0 |
| CVC4 | 0 | 2975 | 556071.931 | 555811.104 | 2975 | 1680 | 1295 | 374 | 373 | 0 |
| z3n | 0 | 2960 | 642715.522 | 642730.816 | 2960 | 1794 | 1166 | 389 | 360 | 0 |
| Yices2 | 0 | 2946 | 535317.786 | 535344.378 | 2946 | 1668 | 1278 | 403 | 403 | 0 |
| Yices2-fixedn | 0 | 2945 | 535720.247 | 535638.564 | 2945 | 1667 | 1278 | 404 | 404 | 0 |
| MathSAT5n | 0 | 2900 | 802793.408 | 802697.395 | 2900 | 1636 | 1264 | 449 | 449 | 0 |
| SMTInterpol | 0 | 2709 | 986539.679 | 936116.52 | 2709 | 1401 | 1308 | 640 | 640 | 0 |
| SMTInterpol-fixedn | 0 | 2709 | 987005.048 | 936583.332 | 2709 | 1401 | 1308 | 640 | 640 | 0 |
| veriT | 0 | 1429 | 1755021.97 | 1755107.492 | 1429 | 936 | 493 | 1913 | 1376 | 1 |
| 2019-Z3n | 0 | 739 | 137185.335 | 137147.303 | 739 | 478 | 261 | 95 | 95 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3218 | 675665.113 | 188879.79 | 3218 | 1875 | 1343 | 131 | 131 | 0 |
| CVC4 | 0 | 2975 | 556071.931 | 555811.104 | 2975 | 1680 | 1295 | 374 | 373 | 0 |
| z3n | 0 | 2960 | 642715.522 | 642730.816 | 2960 | 1794 | 1166 | 389 | 360 | 0 |
| Yices2 | 0 | 2946 | 535317.786 | 535344.378 | 2946 | 1668 | 1278 | 403 | 403 | 0 |
| Yices2-fixedn | 0 | 2945 | 535720.247 | 535638.564 | 2945 | 1667 | 1278 | 404 | 404 | 0 |
| MathSAT5n | 0 | 2900 | 802793.408 | 802697.395 | 2900 | 1636 | 1264 | 449 | 449 | 0 |
| SMTInterpol | 0 | 2709 | 986539.679 | 936116.52 | 2709 | 1401 | 1308 | 640 | 640 | 0 |
| SMTInterpol-fixedn | 0 | 2709 | 987005.048 | 936583.332 | 2709 | 1401 | 1308 | 640 | 640 | 0 |
| veriT | 0 | 1429 | 1755021.97 | 1755107.492 | 1429 | 936 | 493 | 1913 | 1376 | 1 |
| 2019-Z3n | 0 | 739 | 137185.335 | 137147.303 | 739 | 478 | 261 | 95 | 95 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1875 | 251821.349 | 71284.585 | 1875 | 1875 | 0 | 1474 | 131 | 0 |
| z3n | 0 | 1794 | 264330.394 | 264312.807 | 1794 | 1794 | 0 | 1555 | 360 | 0 |
| CVC4 | 0 | 1680 | 357372.183 | 357221.635 | 1680 | 1680 | 0 | 1669 | 373 | 0 |
| Yices2 | 0 | 1668 | 339618.59 | 339633.401 | 1668 | 1668 | 0 | 1681 | 403 | 0 |
| Yices2-fixedn | 0 | 1667 | 339883.643 | 339797.776 | 1667 | 1667 | 0 | 1682 | 404 | 0 |
| MathSAT5n | 0 | 1636 | 457888.483 | 457814.559 | 1636 | 1636 | 0 | 1713 | 449 | 0 |
| SMTInterpol | 0 | 1401 | 761142.178 | 729382.443 | 1401 | 1401 | 0 | 1948 | 640 | 0 |
| SMTInterpol-fixedn | 0 | 1401 | 761474.833 | 729638.668 | 1401 | 1401 | 0 | 1948 | 640 | 0 |
| veriT | 0 | 936 | 911739.367 | 911771.309 | 936 | 936 | 0 | 2406 | 1376 | 1 |
| 2019-Z3n | 0 | 478 | 59803.726 | 59760.161 | 478 | 478 | 0 | 356 | 95 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1343 | 248678.953 | 69591.414 | 1343 | 0 | 1343 | 2006 | 131 | 0 |
| SMTInterpol | 0 | 1308 | 176304.83 | 158732.087 | 1308 | 0 | 1308 | 2041 | 640 | 0 |
| SMTInterpol-fixedn | 0 | 1308 | 176444.046 | 158942.404 | 1308 | 0 | 1308 | 2041 | 640 | 0 |
| CVC4 | 0 | 1295 | 150705.749 | 150587.569 | 1295 | 0 | 1295 | 2054 | 373 | 0 |
| Yices2 | 0 | 1278 | 147703.056 | 147709.176 | 1278 | 0 | 1278 | 2071 | 403 | 0 |
| Yices2-fixedn | 0 | 1278 | 147839.874 | 147839.338 | 1278 | 0 | 1278 | 2071 | 404 | 0 |
| MathSAT5n | 0 | 1264 | 296911.164 | 296881.326 | 1264 | 0 | 1264 | 2085 | 449 | 0 |
| z3n | 0 | 1166 | 330389.909 | 330416.279 | 1166 | 0 | 1166 | 2183 | 360 | 0 |
| veriT | 0 | 493 | 794085.873 | 794134.803 | 493 | 0 | 493 | 2849 | 1376 | 1 |
| 2019-Z3n | 0 | 261 | 44983.279 | 44986.262 | 261 | 0 | 261 | 573 | 95 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3082 | 15099.144 | 9394.245 | 3082 | 1784 | 1298 | 267 | 267 | 0 |
| Yices2 | 0 | 2732 | 18509.634 | 18488.277 | 2732 | 1497 | 1235 | 617 | 617 | 0 |
| Yices2-fixedn | 0 | 2731 | 18536.351 | 18499.031 | 2731 | 1496 | 1235 | 618 | 618 | 0 |
| CVC4 | 0 | 2249 | 37548.021 | 37348.516 | 2249 | 1235 | 1014 | 1100 | 1100 | 0 |
| z3n | 0 | 2134 | 35075.4 | 35002.115 | 2134 | 1270 | 864 | 1215 | 1186 | 0 |
| MathSAT5n | 0 | 1856 | 40688.231 | 40647.285 | 1856 | 1078 | 778 | 1493 | 1493 | 0 |
| SMTInterpol | 0 | 1566 | 60386.234 | 50400.021 | 1566 | 787 | 779 | 1783 | 1783 | 0 |
| SMTInterpol-fixedn | 0 | 1564 | 60297.25 | 50407.615 | 1564 | 784 | 780 | 1785 | 1785 | 0 |
| veriT | 0 | 1118 | 44122.797 | 44087.634 | 1118 | 695 | 423 | 2224 | 1723 | 1 |
| 2019-Z3n | 0 | 623 | 6747.046 | 6695.638 | 623 | 403 | 220 | 211 | 211 | 0 |
n Non-competing.