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 Cloud Track.
Page generated on 2022-08-10 14:49:53 +0000
Benchmarks: 84 Time Limit: 1200 seconds Memory Limit: N/A GB
Logics: This track is experimental. Solvers are only ranked by performance, but no winner is selected.
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| SMTS cube-and-conquer (fixed) | 54 | 17 | 49032.798 | 17 | 13 | 4 | 72 | -5 | 0 | 0 |
| SMTS portfolio | 57 | 14 | 43800.367 | 14 | 14 | 0 | 75 | -5 | 0 | 0 |
| cvc5-cloud | 59 | 10 | 91543.085 | 10 | 3 | 7 | 79 | -5 | 0 | 0 |
| SMTS cube-and-conquer | 60 | 9 | 43366.516 | 9 | 9 | 0 | 80 | -5 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| SMTS cube-and-conquer (fixed) | 28 | 13 | 19689.653 | 13 | 13 | 0 | 32 | 39 | 0 | 0 |
| SMTS portfolio | 30 | 14 | 17926.688 | 14 | 14 | 0 | 31 | 39 | 0 | 0 |
| SMTS cube-and-conquer | 33 | 9 | 19279.329 | 9 | 9 | 0 | 36 | 39 | 0 | 0 |
| cvc5-cloud | 34 | 3 | 50734.59 | 3 | 3 | 0 | 42 | 39 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5-cloud | 25 | 7 | 26408.495 | 7 | 0 | 7 | 25 | 52 | 0 | 0 |
| SMTS cube-and-conquer (fixed) | 26 | 4 | 18015.745 | 4 | 0 | 4 | 28 | 52 | 0 | 0 |
| SMTS cube-and-conquer | 27 | 0 | 17893.653 | 0 | 0 | 0 | 32 | 52 | 0 | 0 |
| SMTS portfolio | 27 | 0 | 20854.868 | 0 | 0 | 0 | 32 | 52 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5-cloud | 4 | 5 | 1958.125 | 5 | 0 | 5 | 84 | -5 | 80 | 0 |
| SMTS portfolio | 6 | 11 | 1989.696 | 11 | 11 | 0 | 78 | -5 | 68 | 0 |
| SMTS cube-and-conquer (fixed) | 7 | 9 | 2010.263 | 9 | 9 | 0 | 80 | -5 | 71 | 0 |
| SMTS cube-and-conquer | 7 | 5 | 2028.707 | 5 | 5 | 0 | 84 | -5 | 73 | 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.