The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 1638 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | Vampire | CVC4 | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 1383 | 581043.979 | 587924.149 | 1383 | 137 | 1246 | 255 | 231 | 0 | |
| CVC4-SymBreakn | 0 | 1381 | 596278.608 | 607017.882 | 1381 | 137 | 1244 | 257 | 231 | 0 | |
| CVC4 | 0 | 1381 | 604438.313 | 617291.032 | 1381 | 137 | 1244 | 257 | 231 | 0 | |
| Vampire | 0 | 1375 | 640132.477 | 624671.324 | 1375 | 99 | 1276 | 263 | 258 | 0 | |
| Z3n | 0 | 1300 | 674937.988 | 677221.993 | 1300 | 155 | 1145 | 338 | 201 | 24 | |
| Alt-Ergo | 0 | 1217 | 758501.014 | 736654.555 | 1217 | 0 | 1217 | 421 | 265 | 38 | |
| veriT | 0 | 1169 | 766139.798 | 766183.373 | 1169 | 0 | 1169 | 469 | 287 | 15 | |
| SMTInterpol | 0 | 893 | 1652269.898 | 1630275.951 | 893 | 93 | 800 | 745 | 665 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 14 | 166473.705 | 162509.338 | 14 | 5 | 9 | 1624 | 65 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 13 | 166768.621 | 162412.582 | 13 | 4 | 9 | 1625 | 65 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 7 | 166646.497 | 162887.45 | 7 | 3 | 4 | 1631 | 65 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 1383 | 587410.849 | 587913.969 | 1383 | 137 | 1246 | 255 | 231 | 0 | |
| Vampire | 0 | 1382 | 687185.437 | 616673.981 | 1382 | 99 | 1283 | 256 | 251 | 0 | |
| CVC4-SymBreakn | 0 | 1381 | 606248.838 | 607006.612 | 1381 | 137 | 1244 | 257 | 231 | 0 | |
| CVC4 | 0 | 1381 | 616468.103 | 617280.482 | 1381 | 137 | 1244 | 257 | 231 | 0 | |
| Z3n | 0 | 1300 | 675012.238 | 677212.773 | 1300 | 155 | 1145 | 338 | 201 | 24 | |
| Alt-Ergo | 0 | 1229 | 794253.464 | 720273.105 | 1229 | 0 | 1229 | 409 | 253 | 38 | |
| veriT | 0 | 1169 | 766211.978 | 766171.143 | 1169 | 0 | 1169 | 469 | 287 | 15 | |
| SMTInterpol | 0 | 895 | 1732196.198 | 1620506.261 | 895 | 93 | 802 | 743 | 638 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 14 | 196335.485 | 157729.655 | 14 | 5 | 9 | 1624 | 57 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 13 | 177996.481 | 158154.92 | 13 | 4 | 9 | 1625 | 60 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 7 | 173572.937 | 158938.424 | 7 | 3 | 4 | 1631 | 61 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 155 | 23734.079 | 23735.2 | 155 | 155 | 0 | 1483 | 201 | 24 |
| 2018-CVC4n | 0 | 137 | 31376.654 | 31565.323 | 137 | 137 | 0 | 1501 | 231 | 0 |
| CVC4-SymBreakn | 0 | 137 | 37956.09 | 38259.261 | 137 | 137 | 0 | 1501 | 231 | 0 |
| CVC4 | 0 | 137 | 46160.614 | 46551.509 | 137 | 137 | 0 | 1501 | 231 | 0 |
| Vampire | 0 | 99 | 163680.17 | 156126.925 | 99 | 99 | 0 | 1539 | 251 | 0 |
| SMTInterpol | 0 | 93 | 60868.764 | 56093.476 | 93 | 93 | 0 | 1545 | 638 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 5 | 7031.341 | 4746.39 | 5 | 5 | 0 | 1633 | 57 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 4 | 7614.865 | 4559.691 | 4 | 4 | 0 | 1634 | 60 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 3 | 6989.379 | 4992.815 | 3 | 3 | 0 | 1635 | 61 | 0 |
| veriT | 0 | 0 | 87096.153 | 87090.078 | 0 | 0 | 0 | 1638 | 287 | 15 |
| Alt-Ergo | 0 | 0 | 142781.919 | 142643.528 | 0 | 0 | 0 | 1638 | 253 | 38 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1283 | 86193.496 | 46991.541 | 1283 | 0 | 1283 | 355 | 251 | 0 |
| 2018-CVC4n | 0 | 1246 | 138434.195 | 138748.646 | 1246 | 0 | 1246 | 392 | 231 | 0 |
| CVC4-SymBreakn | 0 | 1244 | 150692.748 | 151147.351 | 1244 | 0 | 1244 | 394 | 231 | 0 |
| CVC4 | 0 | 1244 | 152707.489 | 153128.973 | 1244 | 0 | 1244 | 394 | 231 | 0 |
| Alt-Ergo | 0 | 1229 | 248456.484 | 182814.691 | 1229 | 0 | 1229 | 409 | 253 | 38 |
| veriT | 0 | 1169 | 310293.021 | 310255.595 | 1169 | 0 | 1169 | 469 | 287 | 15 |
| Z3n | 0 | 1145 | 290572.637 | 292456.469 | 1145 | 0 | 1145 | 493 | 201 | 24 |
| SMTInterpol | 0 | 802 | 1267718.696 | 1181493.656 | 802 | 0 | 802 | 836 | 638 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 9 | 108577.91 | 88421.65 | 9 | 0 | 9 | 1629 | 57 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 9 | 97069.412 | 88808.782 | 9 | 0 | 9 | 1629 | 60 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 4 | 97292.151 | 88767.632 | 4 | 0 | 4 | 1634 | 61 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1351 | 9527.331 | 7707.288 | 1351 | 99 | 1252 | 287 | 287 | 0 | |
| Z3n | 0 | 1271 | 9222.71 | 9222.746 | 1271 | 155 | 1116 | 367 | 342 | 24 | |
| 2018-CVC4n | 0 | 1239 | 9636.401 | 9635.936 | 1239 | 87 | 1152 | 399 | 391 | 0 | |
| CVC4-SymBreakn | 0 | 1236 | 9695.328 | 9694.848 | 1236 | 88 | 1148 | 402 | 394 | 0 | |
| CVC4 | 0 | 1235 | 9705.25 | 9704.786 | 1235 | 88 | 1147 | 403 | 395 | 0 | |
| Alt-Ergo | 0 | 1165 | 10881.024 | 9272.146 | 1165 | 0 | 1165 | 473 | 322 | 38 | |
| veriT | 0 | 1108 | 10066.745 | 10049.121 | 1108 | 0 | 1108 | 530 | 365 | 15 | |
| SMTInterpol | 0 | 823 | 20632.697 | 19458.572 | 823 | 93 | 730 | 815 | 754 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 14 | 7675.815 | 5595.368 | 14 | 5 | 9 | 1624 | 83 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 13 | 7663.916 | 5823.054 | 13 | 4 | 9 | 1625 | 82 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 7 | 7559.95 | 5793.901 | 7 | 3 | 4 | 1631 | 81 | 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.