The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDT division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 1547 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | Alt-Ergo |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 531 | 2530904.251 | 2572747.267 | 531 | 119 | 412 | 1016 | 1016 | 0 | |
| 2018-CVC4n | 0 | 524 | 2501494.731 | 2524970.857 | 524 | 117 | 407 | 1023 | 1023 | 0 | |
| Vampire | 0 | 415 | 2815750.367 | 2741769.393 | 415 | 57 | 358 | 1132 | 1132 | 0 | |
| Alt-Ergo | 0 | 358 | 2688207.92 | 2671802.402 | 358 | 0 | 358 | 1189 | 1061 | 49 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 531 | 2569194.511 | 2572700.617 | 531 | 119 | 412 | 1016 | 1016 | 0 | |
| 2018-CVC4n | 0 | 524 | 2522848.211 | 2524926.067 | 524 | 117 | 407 | 1023 | 1023 | 0 | |
| Vampire | 0 | 434 | 3060141.567 | 2718249.807 | 434 | 58 | 376 | 1113 | 1113 | 0 | |
| Alt-Ergo | 0 | 372 | 2876046.16 | 2652558.061 | 372 | 0 | 372 | 1175 | 1046 | 49 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 119 | 187244.669 | 190394.12 | 119 | 119 | 0 | 1428 | 1016 | 0 |
| 2018-CVC4n | 0 | 117 | 140962.56 | 142742.238 | 117 | 117 | 0 | 1430 | 1023 | 0 |
| Vampire | 0 | 58 | 296449.028 | 245203.067 | 58 | 58 | 0 | 1489 | 1113 | 0 |
| Alt-Ergo | 0 | 0 | 250175.238 | 231943.874 | 0 | 0 | 0 | 1547 | 1046 | 49 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 412 | 113949.842 | 114306.496 | 412 | 0 | 412 | 1135 | 1016 | 0 |
| 2018-CVC4n | 0 | 407 | 113885.651 | 114183.83 | 407 | 0 | 407 | 1140 | 1023 | 0 |
| Vampire | 0 | 376 | 330089.529 | 205198.92 | 376 | 0 | 376 | 1171 | 1113 | 0 |
| Alt-Ergo | 0 | 372 | 280927.181 | 199851.698 | 372 | 0 | 372 | 1175 | 1046 | 49 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Alt-Ergo | 0 | 337 | 29045.785 | 27809.545 | 337 | 0 | 337 | 1210 | 1090 | 49 | |
| 2018-CVC4n | 0 | 327 | 29573.65 | 29573.583 | 327 | 3 | 324 | 1220 | 1220 | 0 | |
| CVC4 | 0 | 326 | 29551.074 | 29550.992 | 326 | 3 | 323 | 1221 | 1221 | 0 | |
| Vampire | 0 | 277 | 35508.944 | 31772.901 | 277 | 0 | 277 | 1270 | 1270 | 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.