The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UF logic in the Unsat Core Track.
Page generated on 2023-07-06 16:05:43 +0000
Benchmarks: 1826 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5 | 0 | 486939 | 8018.091 | 7975.674 | 220 | 0 |
| 2020-CVC4-ucn | 0 | 485447 | 9012.767 | 8969.792 | 243 | 0 |
| 2022-Vampiren | 0 | 479413 | 51116.663 | 13049.346 | 174 | 0 |
| Vampire | 0 | 388228 | 23223.005 | 5984.715 | 186 | 0 |
| SMTInterpol | 0 | 284562 | 57474.433 | 44171.219 | 860 | 0 |
| Yices2 | 0 | 0 | 0.0 | 0.0 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| 2022-Vampiren | 0 | 492157 | 154689.313 | 39095.993 | 133 | 0 |
| cvc5 | 0 | 486939 | 8018.091 | 7975.674 | 220 | 0 |
| 2020-CVC4-ucn | 0 | 485447 | 9012.767 | 8969.792 | 243 | 0 |
| Vampire | 0 | 398845 | 117085.715 | 29574.564 | 127 | 0 |
| SMTInterpol | 0 | 286666 | 66905.273 | 49957.716 | 822 | 0 |
| Yices2 | 0 | 0 | 0.0 | 0.0 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.