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 2020-07-04 11:46:59 +0000
Benchmarks: 2508 Time Limit: 1200 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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2447 | 93732.847 | 80352.617 | 2447 | 1376 | 1071 | 61 | 61 | 0 | |
| MathSAT5n | 0 | 2329 | 443942.69 | 443796.202 | 2329 | 1309 | 1020 | 179 | 179 | 0 | |
| CVC4 | 0 | 2290 | 318190.742 | 317946.291 | 2290 | 1256 | 1034 | 218 | 217 | 0 | |
| z3n | 0 | 2233 | 519173.25 | 519200.236 | 2233 | 1311 | 922 | 275 | 275 | 0 | |
| Yices2 | 0 | 2198 | 410092.801 | 410107.013 | 2198 | 1181 | 1017 | 310 | 310 | 0 | |
| Yices2-fixedn | 0 | 2197 | 410250.569 | 410171.974 | 2197 | 1180 | 1017 | 311 | 311 | 0 | |
| SMTInterpol | 0 | 2170 | 555671.409 | 527233.967 | 2170 | 1097 | 1073 | 338 | 338 | 0 | |
| SMTInterpol-fixedn | 0 | 2168 | 555846.38 | 527576.243 | 2168 | 1095 | 1073 | 340 | 340 | 0 | |
| veriT | 0 | 819 | 1433613.127 | 1433714.083 | 819 | 574 | 245 | 1689 | 1152 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2459 | 103682.297 | 74071.798 | 2459 | 1384 | 1075 | 49 | 49 | 0 | |
| MathSAT5n | 0 | 2329 | 443971.89 | 443789.002 | 2329 | 1309 | 1020 | 179 | 179 | 0 | |
| CVC4 | 0 | 2290 | 318208.962 | 317939.421 | 2290 | 1256 | 1034 | 218 | 217 | 0 | |
| z3n | 0 | 2233 | 519201.44 | 519189.756 | 2233 | 1311 | 922 | 275 | 275 | 0 | |
| Yices2 | 0 | 2198 | 410115.181 | 410099.193 | 2198 | 1181 | 1017 | 310 | 310 | 0 | |
| Yices2-fixedn | 0 | 2197 | 410271.249 | 410163.744 | 2197 | 1180 | 1017 | 311 | 311 | 0 | |
| SMTInterpol | 0 | 2170 | 555671.409 | 527233.967 | 2170 | 1097 | 1073 | 338 | 338 | 0 | |
| SMTInterpol-fixedn | 0 | 2170 | 555863.97 | 527552.913 | 2170 | 1097 | 1073 | 338 | 338 | 0 | |
| veriT | 0 | 819 | 1433703.647 | 1433672.183 | 819 | 574 | 245 | 1689 | 1152 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1384 | 51796.307 | 31039.904 | 1384 | 1384 | 0 | 1124 | 49 | 0 |
| z3n | 0 | 1311 | 215944.195 | 215929.51 | 1311 | 1311 | 0 | 1197 | 275 | 0 |
| MathSAT5n | 0 | 1309 | 200590.763 | 200464.602 | 1309 | 1309 | 0 | 1199 | 179 | 0 |
| CVC4 | 0 | 1256 | 206924.201 | 206786.28 | 1256 | 1256 | 0 | 1252 | 217 | 0 |
| Yices2 | 0 | 1181 | 295917.05 | 295908.892 | 1181 | 1181 | 0 | 1327 | 310 | 0 |
| Yices2-fixedn | 0 | 1180 | 296110.789 | 296014.219 | 1180 | 1180 | 0 | 1328 | 311 | 0 |
| SMTInterpol | 0 | 1097 | 454690.446 | 440009.694 | 1097 | 1097 | 0 | 1411 | 338 | 0 |
| SMTInterpol-fixedn | 0 | 1097 | 454844.083 | 440201.975 | 1097 | 1097 | 0 | 1411 | 338 | 0 |
| veriT | 0 | 574 | 683786.095 | 683777.036 | 574 | 574 | 0 | 1934 | 1152 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1075 | 36285.99 | 27431.894 | 1075 | 0 | 1075 | 1433 | 49 | 0 |
| SMTInterpol | 0 | 1073 | 85380.963 | 71624.273 | 1073 | 0 | 1073 | 1435 | 338 | 0 |
| SMTInterpol-fixedn | 0 | 1073 | 85419.887 | 71750.938 | 1073 | 0 | 1073 | 1435 | 338 | 0 |
| CVC4 | 0 | 1034 | 95684.761 | 95553.142 | 1034 | 0 | 1034 | 1474 | 217 | 0 |
| MathSAT5n | 0 | 1020 | 227781.127 | 227724.4 | 1020 | 0 | 1020 | 1488 | 179 | 0 |
| Yices2-fixedn | 0 | 1017 | 98560.46 | 98549.525 | 1017 | 0 | 1017 | 1491 | 311 | 0 |
| Yices2 | 0 | 1017 | 98598.131 | 98590.301 | 1017 | 0 | 1017 | 1491 | 310 | 0 |
| z3n | 0 | 922 | 287657.245 | 287660.247 | 922 | 0 | 922 | 1586 | 275 | 0 |
| veriT | 0 | 245 | 734317.552 | 734295.147 | 245 | 0 | 245 | 2263 | 1152 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2405 | 7636.104 | 4497.818 | 2405 | 1345 | 1060 | 103 | 103 | 0 | |
| Yices2 | 0 | 2057 | 13494.279 | 13474.497 | 2057 | 1057 | 1000 | 451 | 451 | 0 | |
| Yices2-fixedn | 0 | 2057 | 13505.262 | 13484.435 | 2057 | 1057 | 1000 | 451 | 451 | 0 | |
| CVC4 | 0 | 1797 | 26411.213 | 26223.854 | 1797 | 994 | 803 | 711 | 711 | 0 | |
| z3n | 0 | 1524 | 28434.148 | 28386.278 | 1524 | 864 | 660 | 984 | 984 | 0 | |
| MathSAT5n | 0 | 1408 | 29959.777 | 29920.814 | 1408 | 850 | 558 | 1100 | 1100 | 0 | |
| SMTInterpol | 0 | 1216 | 45067.936 | 37042.005 | 1216 | 615 | 601 | 1292 | 1292 | 0 | |
| SMTInterpol-fixedn | 0 | 1213 | 44972.826 | 37049.903 | 1213 | 612 | 601 | 1295 | 1295 | 0 | |
| veriT | 0 | 703 | 33101.615 | 33066.388 | 703 | 500 | 203 | 1805 | 1304 | 1 |
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.