The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality+LinearArith division in the Incremental Track.
Page generated on 2021-07-18 17:30:28 +0000
Benchmarks: 2031 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| cvc5-inc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| 2020-z3n | 0 | 5673796 | 106126.094 | 105517.182 | 64665 | 0 | 68 | 0 |
| z3n | 0 | 5547234 | 230193.276 | 229737.609 | 191227 | 0 | 150 | 0 |
| cvc5-inc | 0 | 4918703 | 175424.176 | 174391.546 | 819758 | 0 | 103 | 0 |
| SMTInterpol | 0 | 4816541 | 204729.747 | 188208.149 | 921920 | 0 | 122 | 0 |
| 2018-Yices (incremental)n | 0 | 4699864 | 3249.849 | 3040.414 | 0 | 0 | 0 | 0 |
| Yices2 incremental | 0 | 4079606 | 112597.221 | 112010.018 | 1658855 | 0 | 77 | 0 |
| MathSAT5n | 0 | 3050382 | 145383.663 | 144812.887 | 2688079 | 0 | 105 | 0 |
| 2018-Z3 (incremental)n | 0 | 1020534 | 84331.722 | 84219.446 | 4958 | 0 | 62 | 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.