The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearIntArith division in the Incremental Track.
Page generated on 2021-07-18 17:30:28 +0000
Benchmarks: 69 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| Yices2 incremental |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Yices2 incremental | 0 | 20040333 | 32658.648 | 32143.399 | 881 | 0 | 20 | 0 |
| 2020-Yices2-fixed incrementaln | 0 | 20040331 | 32277.5 | 31765.378 | 883 | 0 | 20 | 0 |
| z3n | 0 | 19664650 | 52836.174 | 52265.011 | 376564 | 0 | 32 | 0 |
| MathSAT5n | 0 | 17407412 | 40936.744 | 40460.088 | 2633802 | 0 | 26 | 0 |
| SMTInterpol | 0 | 16702620 | 58238.615 | 55490.574 | 3338594 | 0 | 37 | 0 |
| cvc5-inc | 0 | 7389770 | 60927.573 | 60812.936 | 12651444 | 0 | 44 | 0 |
| OpenSMT | 0 | 593412 | 61481.403 | 62070.44 | 19447802 | 0 | 47 | 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.