The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality+NonLinearArith division in the Incremental Track.
Page generated on 2021-07-18 17:30:28 +0000
Benchmarks: 512 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| SMTInterpol |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 150310 | 164.795 | 154.451 | 2 | 0 | 0 | 0 |
| SMTInterpol | 0 | 148218 | 1851.736 | 719.86 | 2094 | 0 | 0 | 0 |
| cvc5-inc | 0 | 142017 | 2525.048 | 2507.305 | 8295 | 0 | 1 | 0 |
| 2020-MathSAT5n | 0 | 96674 | 92.598 | 57.037 | 53632 | 0 | 0 | 0 |
| MathSAT5n | 0 | 96674 | 56.069 | 59.051 | 53638 | 0 | 0 | 0 |
| Yices2 incremental | 0 | 19180 | 1201.749 | 1205.962 | 79402 | 0 | 1 | 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.