The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearRealArith division in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 196 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 146557 | 68745.629 | 68695.713 | 37 | 0 | |
| Yices2 | 0 | 140760 | 80304.012 | 80297.183 | 47 | 0 | |
| cvc5-uc | 0 | 138734 | 45084.307 | 45091.443 | 14 | 0 | |
| z3n | 0 | 118077 | 73539.143 | 73438.998 | 33 | 0 | |
| MathSAT5n | 0 | 115011 | 146153.994 | 146181.835 | 106 | 0 | |
| SMTInterpol | 0 | 93971 | 107306.53 | 103552.672 | 52 | 0 | |
| SMTInterpol-remus | 0 | 75322 | 158746.624 | 154062.19 | 69 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 146557 | 68749.059 | 68694.633 | 37 | 0 | |
| Yices2 | 0 | 140760 | 80307.662 | 80295.823 | 47 | 0 | |
| cvc5-uc | 0 | 138734 | 45086.497 | 45090.853 | 14 | 0 | |
| z3n | 0 | 118077 | 73541.293 | 73438.098 | 33 | 0 | |
| MathSAT5n | 0 | 115011 | 146173.094 | 146176.625 | 106 | 0 | |
| SMTInterpol | 0 | 94356 | 107328.87 | 103543.272 | 51 | 0 | |
| SMTInterpol-remus | 0 | 80954 | 158919.954 | 153154.58 | 53 | 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.