The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 3136 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3072 | 197764.078 | 168700.961 | 3072 | 1729 | 1343 | 64 | 64 | 0 | |
| SPASS-SATT | 0 | 3048 | 282189.257 | 281995.245 | 3048 | 1713 | 1335 | 88 | 84 | 4 | |
| 2018-SPASS-SATTn | 0 | 3045 | 295055.067 | 294911.347 | 3045 | 1717 | 1328 | 91 | 87 | 4 | |
| Z3n | 0 | 2946 | 549287.73 | 549177.789 | 2946 | 1663 | 1283 | 190 | 190 | 0 | |
| CVC4 | 0 | 2841 | 783304.577 | 783176.221 | 2841 | 1549 | 1292 | 295 | 292 | 0 | |
| Ctrl-Ergo | 0 | 2797 | 1033195.356 | 867421.359 | 2797 | 1523 | 1274 | 339 | 134 | 204 | |
| Yices 2.6.2 | 0 | 2744 | 1050186.26 | 1050208.801 | 2744 | 1476 | 1268 | 392 | 392 | 0 | |
| SMTInterpol | 0 | 2734 | 1205032.684 | 1171829.842 | 2734 | 1402 | 1332 | 402 | 402 | 0 | |
| CVC4-SymBreakn | 0 | 2646 | 1307242.706 | 1328980.076 | 2646 | 1362 | 1284 | 490 | 490 | 0 | |
| veriT | 0 | 1113 | 3338624.715 | 3338782.703 | 1113 | 734 | 379 | 2023 | 1324 | 1 | |
| ProB | 0 | 274 | 6591657.04 | 6592372.087 | 274 | 182 | 92 | 2862 | 2718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3086 | 215147.668 | 152103.196 | 3086 | 1738 | 1348 | 50 | 50 | 0 | |
| SPASS-SATT | 0 | 3048 | 282208.177 | 281992.165 | 3048 | 1713 | 1335 | 88 | 84 | 4 | |
| 2018-SPASS-SATTn | 0 | 3045 | 295076.397 | 294907.477 | 3045 | 1717 | 1328 | 91 | 87 | 4 | |
| Z3n | 0 | 2946 | 549320.08 | 549170.529 | 2946 | 1663 | 1283 | 190 | 190 | 0 | |
| CVC4 | 0 | 2841 | 783358.407 | 783165.991 | 2841 | 1549 | 1292 | 295 | 292 | 0 | |
| Ctrl-Ergo | 0 | 2833 | 1124939.326 | 825874.026 | 2833 | 1534 | 1299 | 303 | 98 | 204 | |
| Yices 2.6.2 | 0 | 2744 | 1050239.29 | 1050196.301 | 2744 | 1476 | 1268 | 392 | 392 | 0 | |
| SMTInterpol | 0 | 2736 | 1205091.524 | 1171803.842 | 2736 | 1404 | 1332 | 400 | 400 | 0 | |
| CVC4-SymBreakn | 0 | 2646 | 1321757.416 | 1328960.066 | 2646 | 1362 | 1284 | 490 | 490 | 0 | |
| veriT | 0 | 1113 | 3338791.785 | 3338736.023 | 1113 | 734 | 379 | 2023 | 1324 | 1 | |
| ProB | 0 | 274 | 6591933.66 | 6592287.157 | 274 | 182 | 92 | 2862 | 2718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1738 | 126913.526 | 82532.942 | 1738 | 1738 | 0 | 1398 | 50 | 0 |
| 2018-SPASS-SATTn | 0 | 1717 | 162084.481 | 161997.841 | 1717 | 1717 | 0 | 1419 | 87 | 4 |
| SPASS-SATT | 0 | 1713 | 165675.025 | 165605.88 | 1713 | 1713 | 0 | 1423 | 84 | 4 |
| Z3n | 0 | 1663 | 297488.335 | 297371.503 | 1663 | 1663 | 0 | 1473 | 190 | 0 |
| CVC4 | 0 | 1549 | 567155.175 | 567059.03 | 1549 | 1549 | 0 | 1587 | 292 | 0 |
| Ctrl-Ergo | 0 | 1534 | 750026.962 | 600208.104 | 1534 | 1534 | 0 | 1602 | 98 | 204 |
| Yices 2.6.2 | 0 | 1476 | 775889.037 | 775879.677 | 1476 | 1476 | 0 | 1660 | 392 | 0 |
| SMTInterpol | 0 | 1404 | 1045151.738 | 1027742.584 | 1404 | 1404 | 0 | 1732 | 400 | 0 |
| CVC4-SymBreakn | 0 | 1362 | 1061142.277 | 1064058.292 | 1362 | 1362 | 0 | 1774 | 490 | 0 |
| veriT | 0 | 734 | 1606797.554 | 1606762.357 | 734 | 734 | 0 | 2402 | 1324 | 1 |
| ProB | 0 | 182 | 3585929.583 | 3586284.736 | 182 | 182 | 0 | 2954 | 2718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1348 | 52234.142 | 33570.254 | 1348 | 0 | 1348 | 1788 | 50 | 0 |
| SPASS-SATT | 0 | 1335 | 80533.152 | 80386.286 | 1335 | 0 | 1335 | 1801 | 84 | 4 |
| SMTInterpol | 0 | 1332 | 123939.786 | 108061.258 | 1332 | 0 | 1332 | 1804 | 400 | 0 |
| 2018-SPASS-SATTn | 0 | 1328 | 96991.916 | 96909.636 | 1328 | 0 | 1328 | 1808 | 87 | 4 |
| Ctrl-Ergo | 0 | 1299 | 338912.363 | 189665.922 | 1299 | 0 | 1299 | 1837 | 98 | 204 |
| CVC4 | 0 | 1292 | 180203.232 | 180106.96 | 1292 | 0 | 1292 | 1844 | 292 | 0 |
| CVC4-SymBreakn | 0 | 1284 | 224615.139 | 228901.774 | 1284 | 0 | 1284 | 1852 | 490 | 0 |
| Z3n | 0 | 1283 | 215831.745 | 215799.026 | 1283 | 0 | 1283 | 1853 | 190 | 0 |
| Yices 2.6.2 | 0 | 1268 | 238350.253 | 238316.624 | 1268 | 0 | 1268 | 1868 | 392 | 0 |
| veriT | 0 | 379 | 1695994.231 | 1695973.666 | 379 | 0 | 379 | 2757 | 1324 | 1 |
| ProB | 0 | 92 | 2970004.078 | 2970002.421 | 92 | 0 | 92 | 3044 | 2718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2994 | 9534.185 | 5822.129 | 2994 | 1665 | 1329 | 142 | 142 | 0 | |
| SPASS-SATT | 0 | 2527 | 23562.509 | 23409.786 | 2527 | 1458 | 1069 | 609 | 605 | 4 | |
| Yices 2.6.2 | 0 | 2526 | 17620.525 | 17568.902 | 2526 | 1288 | 1238 | 610 | 610 | 0 | |
| 2018-SPASS-SATTn | 0 | 2450 | 24081.823 | 24004.924 | 2450 | 1403 | 1047 | 686 | 682 | 4 | |
| Z3n | 0 | 2329 | 26796.696 | 26776.302 | 2329 | 1280 | 1049 | 807 | 807 | 0 | |
| Ctrl-Ergo | 0 | 2301 | 46909.169 | 27051.212 | 2301 | 1208 | 1093 | 835 | 630 | 204 | |
| CVC4 | 0 | 2281 | 31332.521 | 31250.872 | 2281 | 1229 | 1052 | 855 | 855 | 0 | |
| SMTInterpol | 0 | 1651 | 56168.719 | 44749.132 | 1651 | 818 | 833 | 1485 | 1485 | 0 | |
| CVC4-SymBreakn | 0 | 1332 | 49175.502 | 49124.765 | 1332 | 628 | 704 | 1804 | 1804 | 0 | |
| veriT | 0 | 902 | 40494.275 | 40454.038 | 902 | 617 | 285 | 2234 | 1576 | 1 | |
| ProB | 0 | 186 | 69048.47 | 69050.513 | 186 | 132 | 54 | 2950 | 2833 | 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.