The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 2278 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | SMTInterpol | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1329 | 1154965.807 | 1144351.663 | 1329 | 5 | 1324 | 949 | 907 | 42 | |
| CVC4 | 0 | 1307 | 1166696.778 | 1180752.12 | 1307 | 2 | 1305 | 971 | 955 | 0 | |
| veriT | 0 | 1263 | 1242519.129 | 1242652.094 | 1263 | 0 | 1263 | 1015 | 972 | 12 | |
| Vampire | 0 | 1223 | 1334156.22 | 1283319.05 | 1223 | 0 | 1223 | 1055 | 1055 | 0 | |
| veriT+viten | 0 | 1206 | 1250242.688 | 1250340.746 | 1206 | 0 | 1206 | 1072 | 1029 | 4 | |
| Alt-Ergo | 0 | 1078 | 1427231.281 | 1392943.906 | 1078 | 0 | 1078 | 1200 | 1129 | 20 | |
| z3n | 0 | 1057 | 1198690.108 | 1201019.438 | 1057 | 5 | 1052 | 1221 | 829 | 9 | |
| SMTInterpol | 0 | 284 | 2333003.764 | 2331054.501 | 284 | 3 | 281 | 1994 | 1938 | 0 | |
| SMTInterpol-fixedn | 0 | 284 | 2333069.191 | 2331097.743 | 284 | 3 | 281 | 1994 | 1938 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 25174.454 | 22529.603 | 0 | 0 | 0 | 2278 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1345 | 1163033.407 | 1134270.494 | 1345 | 7 | 1338 | 933 | 891 | 42 | |
| CVC4 | 0 | 1307 | 1180355.998 | 1180708.28 | 1307 | 2 | 1305 | 971 | 955 | 0 | |
| veriT | 0 | 1263 | 1242635.439 | 1242614.754 | 1263 | 0 | 1263 | 1015 | 972 | 12 | |
| Vampire | 0 | 1255 | 1439814.88 | 1264098.108 | 1255 | 0 | 1255 | 1023 | 1023 | 0 | |
| veriT+viten | 0 | 1206 | 1250335.438 | 1250304.126 | 1206 | 0 | 1206 | 1072 | 1029 | 4 | |
| Alt-Ergo | 0 | 1112 | 1474430.401 | 1370608.812 | 1112 | 0 | 1112 | 1166 | 1094 | 20 | |
| z3n | 0 | 1057 | 1199972.418 | 1200982.668 | 1057 | 5 | 1052 | 1221 | 829 | 9 | |
| SMTInterpol | 0 | 284 | 2342704.484 | 2328601.656 | 284 | 3 | 281 | 1994 | 1931 | 0 | |
| SMTInterpol-fixedn | 0 | 284 | 2346851.701 | 2328906.414 | 284 | 3 | 281 | 1994 | 1930 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 25174.454 | 22529.603 | 0 | 0 | 0 | 2278 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7 | 4117.96 | 2176.631 | 7 | 7 | 0 | 2271 | 891 | 42 |
| z3n | 0 | 5 | 3600.277 | 3600.277 | 5 | 5 | 0 | 2273 | 829 | 9 |
| SMTInterpol | 0 | 3 | 4803.715 | 4802.048 | 3 | 3 | 0 | 2275 | 1931 | 0 |
| SMTInterpol-fixedn | 0 | 3 | 4803.747 | 4802.086 | 3 | 3 | 0 | 2275 | 1930 | 0 |
| CVC4 | 0 | 2 | 5270.981 | 5279.361 | 2 | 2 | 0 | 2276 | 955 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 27.816 | 19.201 | 0 | 0 | 0 | 2278 | 14 | 0 |
| Alt-Ergo | 0 | 0 | 2401.413 | 2400.493 | 0 | 0 | 0 | 2278 | 1094 | 20 |
| veriT+viten | 0 | 0 | 3010.593 | 3010.698 | 0 | 0 | 0 | 2278 | 1029 | 4 |
| veriT | 0 | 0 | 6921.984 | 6922.379 | 0 | 0 | 0 | 2278 | 972 | 12 |
| Vampire | 0 | 0 | 9600.0 | 9600.0 | 0 | 0 | 0 | 2278 | 1023 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1338 | 104115.447 | 77293.864 | 1338 | 0 | 1338 | 940 | 891 | 42 |
| CVC4 | 0 | 1305 | 134112.021 | 134453.687 | 1305 | 0 | 1305 | 973 | 955 | 0 |
| veriT | 0 | 1263 | 194775.559 | 194751.054 | 1263 | 0 | 1263 | 1015 | 972 | 12 |
| Vampire | 0 | 1255 | 314211.52 | 199752.088 | 1255 | 0 | 1255 | 1023 | 1023 | 0 |
| veriT+viten | 0 | 1206 | 226046.526 | 226014.72 | 1206 | 0 | 1206 | 1072 | 1029 | 4 |
| Alt-Ergo | 0 | 1112 | 451501.515 | 362512.673 | 1112 | 0 | 1112 | 1166 | 1094 | 20 |
| z3n | 0 | 1052 | 344594.655 | 344728.208 | 1052 | 0 | 1052 | 1226 | 829 | 9 |
| SMTInterpol | 0 | 281 | 1341409.22 | 1333181.901 | 281 | 0 | 281 | 1997 | 1931 | 0 |
| SMTInterpol-fixedn | 0 | 281 | 1339373.04 | 1333464.798 | 281 | 0 | 281 | 1997 | 1930 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 21928.031 | 20167.339 | 0 | 0 | 0 | 2278 | 14 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1276 | 25918.42 | 24805.987 | 1276 | 5 | 1271 | 1002 | 960 | 42 | |
| veriT+viten | 0 | 1185 | 27169.124 | 27136.911 | 1185 | 0 | 1185 | 1093 | 1062 | 4 | |
| CVC4 | 0 | 1161 | 28023.312 | 27964.894 | 1161 | 0 | 1161 | 1117 | 1108 | 0 | |
| Vampire | 0 | 1047 | 37735.654 | 31743.184 | 1047 | 0 | 1047 | 1231 | 1231 | 0 | |
| z3n | 0 | 1012 | 31547.757 | 31526.221 | 1012 | 5 | 1007 | 1266 | 1257 | 9 | |
| Alt-Ergo | 0 | 1000 | 38900.417 | 32221.648 | 1000 | 0 | 1000 | 1278 | 1222 | 20 | |
| veriT | 0 | 951 | 32349.708 | 32345.11 | 951 | 0 | 951 | 1327 | 1315 | 12 | |
| SMTInterpol | 0 | 263 | 48976.823 | 47809.23 | 263 | 3 | 260 | 2015 | 1960 | 0 | |
| SMTInterpol-fixedn | 0 | 263 | 48968.879 | 47813.358 | 263 | 3 | 260 | 2015 | 1960 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 8750.685 | 5903.693 | 0 | 0 | 0 | 2278 | 16 | 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.