The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 3311 Time Limit: 1200 seconds Memory Limit: 60 GB
| 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3224 | 137480.246 | 115820.91 | 3224 | 1827 | 1397 | 87 | 87 | 0 |
| MathSAT5n | 0 | 3082 | 536818.171 | 536890.952 | 3082 | 1742 | 1340 | 229 | 229 | 0 |
| cvc5 | 0 | 3001 | 680936.404 | 680832.849 | 3001 | 1655 | 1346 | 310 | 307 | 0 |
| cvc5 - fixedn | 0 | 3001 | 680976.268 | 680853.382 | 3001 | 1655 | 1346 | 310 | 307 | 0 |
| Yices2 | 0 | 2842 | 618215.135 | 618229.051 | 2842 | 1527 | 1315 | 469 | 469 | 0 |
| z3n | 0 | 2829 | 728415.0 | 728725.022 | 2829 | 1626 | 1203 | 482 | 482 | 0 |
| SMTInterpol | 0 | 2490 | 1174514.937 | 1139300.537 | 2490 | 1474 | 1016 | 821 | 821 | 0 |
| OpenSMT - fixedn | 0 | 2339 | 1273659.142 | 1385700.4 | 2339 | 1173 | 1166 | 972 | 457 | 0 |
| veriT | 0 | 1299 | 1980055.096 | 1980192.498 | 1299 | 843 | 456 | 2012 | 1563 | 0 |
| OpenSMT | 8 | 2334 | 1266438.632 | 1380987.735 | 2334 | 1176 | 1158 | 977 | 477 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3245 | 156602.866 | 105403.523 | 3245 | 1843 | 1402 | 66 | 66 | 0 |
| MathSAT5n | 0 | 3082 | 536970.141 | 536881.502 | 3082 | 1742 | 1340 | 229 | 229 | 0 |
| cvc5 | 0 | 3001 | 680962.124 | 680822.989 | 3001 | 1655 | 1346 | 310 | 307 | 0 |
| cvc5 - fixedn | 0 | 3001 | 681001.968 | 680842.722 | 3001 | 1655 | 1346 | 310 | 307 | 0 |
| Yices2 | 0 | 2842 | 618245.555 | 618216.521 | 2842 | 1527 | 1315 | 469 | 469 | 0 |
| z3n | 0 | 2829 | 728690.26 | 728704.812 | 2829 | 1626 | 1203 | 482 | 482 | 0 |
| SMTInterpol | 0 | 2491 | 1174524.867 | 1139164.987 | 2491 | 1475 | 1016 | 820 | 820 | 0 |
| OpenSMT - fixedn | 0 | 2339 | 1299578.052 | 1385681.68 | 2339 | 1173 | 1166 | 972 | 457 | 0 |
| veriT | 0 | 1299 | 1980166.556 | 1980140.878 | 1299 | 843 | 456 | 2012 | 1563 | 0 |
| OpenSMT | 8 | 2334 | 1298731.18 | 1380971.075 | 2334 | 1176 | 1158 | 977 | 478 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1843 | 104257.837 | 64577.148 | 1843 | 1843 | 0 | 37 | 1431 | 66 | 0 |
| MathSAT5n | 0 | 1742 | 278003.608 | 277909.082 | 1742 | 1742 | 0 | 138 | 1431 | 229 | 0 |
| cvc5 | 0 | 1655 | 418306.816 | 418227.79 | 1655 | 1655 | 0 | 225 | 1431 | 307 | 0 |
| cvc5 - fixedn | 0 | 1655 | 418442.901 | 418286.109 | 1655 | 1655 | 0 | 225 | 1431 | 307 | 0 |
| z3n | 0 | 1626 | 413790.05 | 413868.521 | 1626 | 1626 | 0 | 254 | 1431 | 482 | 0 |
| Yices2 | 0 | 1527 | 471192.102 | 471171.038 | 1527 | 1527 | 0 | 353 | 1431 | 469 | 0 |
| SMTInterpol | 0 | 1475 | 619713.965 | 598484.73 | 1475 | 1475 | 0 | 405 | 1431 | 820 | 0 |
| OpenSMT - fixedn | 0 | 1173 | 924678.778 | 1003866.863 | 1173 | 1173 | 0 | 707 | 1431 | 457 | 0 |
| veriT | 0 | 843 | 886446.424 | 886415.676 | 843 | 843 | 0 | 1037 | 1431 | 1563 | 0 |
| OpenSMT | 8 | 1176 | 924117.216 | 999611.17 | 1176 | 1176 | 0 | 704 | 1431 | 478 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1402 | 39145.029 | 27626.375 | 1402 | 0 | 1402 | 18 | 1891 | 66 | 0 |
| cvc5 - fixedn | 0 | 1346 | 249359.067 | 249356.613 | 1346 | 0 | 1346 | 74 | 1891 | 307 | 0 |
| cvc5 | 0 | 1346 | 249455.309 | 249395.198 | 1346 | 0 | 1346 | 74 | 1891 | 307 | 0 |
| MathSAT5n | 0 | 1340 | 245766.532 | 245772.421 | 1340 | 0 | 1340 | 80 | 1891 | 229 | 0 |
| Yices2 | 0 | 1315 | 133853.453 | 133845.483 | 1315 | 0 | 1315 | 105 | 1891 | 469 | 0 |
| z3n | 0 | 1203 | 301700.21 | 301636.291 | 1203 | 0 | 1203 | 217 | 1891 | 482 | 0 |
| OpenSMT - fixedn | 0 | 1166 | 361699.273 | 368614.816 | 1166 | 0 | 1166 | 254 | 1891 | 457 | 0 |
| OpenSMT | 0 | 1158 | 361413.964 | 368159.904 | 1158 | 0 | 1158 | 262 | 1891 | 478 | 0 |
| SMTInterpol | 0 | 1016 | 541610.901 | 527480.257 | 1016 | 0 | 1016 | 404 | 1891 | 820 | 0 |
| veriT | 0 | 456 | 1080520.132 | 1080525.202 | 456 | 0 | 456 | 964 | 1891 | 1563 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3152 | 10270.248 | 6353.096 | 3152 | 1773 | 1379 | 159 | 159 | 0 |
| Yices2 | 0 | 2659 | 18846.004 | 18812.129 | 2659 | 1375 | 1284 | 652 | 652 | 0 |
| z3n | 0 | 2119 | 35415.884 | 35335.449 | 2119 | 1161 | 958 | 1192 | 1192 | 0 |
| MathSAT5n | 0 | 1994 | 36509.845 | 36435.346 | 1994 | 1203 | 791 | 1317 | 1317 | 0 |
| cvc5 | 0 | 1632 | 43844.014 | 43754.037 | 1632 | 959 | 673 | 1679 | 1679 | 0 |
| cvc5 - fixedn | 0 | 1631 | 43821.89 | 43754.436 | 1631 | 959 | 672 | 1680 | 1680 | 0 |
| SMTInterpol | 0 | 1523 | 59858.506 | 50010.059 | 1523 | 859 | 664 | 1788 | 1788 | 0 |
| OpenSMT - fixedn | 0 | 1279 | 55577.394 | 55501.204 | 1279 | 573 | 706 | 2032 | 2028 | 0 |
| veriT | 0 | 1025 | 48910.316 | 48876.015 | 1025 | 698 | 327 | 2286 | 1919 | 0 |
| OpenSMT | 8 | 1275 | 55431.844 | 55378.592 | 1275 | 576 | 699 | 2036 | 2024 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.