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 2021-07-18 17:31:25 +0000
Benchmarks: 1697 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| cvc5-uc | cvc5-uc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 475159 | 151580.315 | 151604.214 | 121 | 0 |
| 2020-CVC4-ucn | 0 | 473850 | 169147.234 | 169181.674 | 133 | 0 |
| z3n | 0 | 392891 | 341085.353 | 341102.384 | 202 | 8 |
| SMTInterpol | 0 | 287674 | 905312.438 | 891617.8 | 713 | 0 |
| SMTInterpol-remus | 0 | 177564 | 1553443.855 | 1491460.168 | 978 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 10956.247 | 6970.185 | 1 | 0 |
| Vampire | 1 | 471070 | 155091.138 | 121066.894 | 91 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 475159 | 151599.385 | 151599.004 | 121 | 0 |
| 2020-CVC4-ucn | 0 | 473850 | 169173.994 | 169175.564 | 133 | 0 |
| z3n | 0 | 392891 | 341122.603 | 341093.494 | 202 | 8 |
| SMTInterpol | 0 | 290423 | 938780.208 | 880134.638 | 684 | 0 |
| SMTInterpol-remus | 0 | 271770 | 1676096.135 | 1452966.131 | 684 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 10956.247 | 6970.185 | 1 | 0 |
| Vampire | 1 | 479804 | 207360.488 | 108122.557 | 61 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.