The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDT logic in the Unsat Core Track.
Page generated on 2023-07-06 16:05:43 +0000
Benchmarks: 1369 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 |
---|---|---|---|---|---|---|
2022-Vampiren | 0 | 338258 | 39241.95 | 10013.873 | 279 | 0 |
cvc5 | 0 | 337860 | 4160.624 | 4156.027 | 328 | 0 |
2020-CVC4-ucn | 0 | 335293 | 6341.638 | 6340.998 | 328 | 0 |
SMTInterpol | 0 | 211526 | 31504.938 | 22244.164 | 691 | 0 |
Vampire | 121 | 341260 | 83369.709 | 21104.767 | 101 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
2022-Vampiren | 0 | 348440 | 121907.77 | 30568.053 | 249 | 0 |
cvc5 | 0 | 337860 | 4160.624 | 4156.027 | 328 | 0 |
2020-CVC4-ucn | 0 | 335293 | 6341.638 | 6340.998 | 328 | 0 |
SMTInterpol | 0 | 212923 | 37717.738 | 25549.173 | 676 | 0 |
Vampire | 121 | 351386 | 201869.109 | 50919.503 | 54 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.