The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA logic in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 3862 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 | 923558 | 174712.363 | 174688.71 | 131 | 0 |
| 2020-CVC4-ucn | 0 | 922036 | 202177.198 | 202177.266 | 154 | 0 |
| 2020-z3n | 0 | 870462 | 270568.604 | 270782.548 | 157 | 6 |
| z3n | 0 | 868471 | 276338.608 | 276321.174 | 157 | 2 |
| Vampire | 0 | 828021 | 309420.654 | 239685.964 | 179 | 0 |
| SMTInterpol | 0 | 597007 | 1641734.328 | 1631418.451 | 1317 | 0 |
| SMTInterpol-remus | 0 | 496919 | 2759845.82 | 2681492.82 | 1706 | 0 |
| UltimateEliminator+MathSAT | 2 | 2443 | 38405.967 | 29421.979 | 11 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 923558 | 174736.093 | 174683.18 | 131 | 0 |
| 2020-CVC4-ucn | 0 | 922036 | 202213.818 | 202170.276 | 154 | 0 |
| 2020-z3n | 0 | 870462 | 270875.024 | 270775.718 | 157 | 6 |
| z3n | 0 | 868471 | 276369.468 | 276314.344 | 157 | 2 |
| Vampire | 0 | 832035 | 364620.884 | 207132.509 | 128 | 0 |
| SMTInterpol | 0 | 598363 | 1662024.268 | 1626806.642 | 1296 | 0 |
| SMTInterpol-remus | 0 | 592103 | 2834085.17 | 2647684.608 | 1303 | 0 |
| UltimateEliminator+MathSAT | 2 | 2443 | 38405.967 | 29421.979 | 11 | 1 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.