The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_UFLIA logic in the Incremental Track. Chart
Results were generated on 2025-08-11
Benchmarks: 386
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|---|---|---|
Yices2 | - | - | Yices2 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Unsolved | Abstained | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|
Yices2 | 0 | 10952 | 75394.20 | 75394.20 | 0 | 386 | 0 | 77 | 0 |
cvc5 | 0 | 9142 | 107826.51 | 107826.51 | 0 | 386 | 0 | 90 | 0 |
SMTInterpol | 0 | 8510 | 77922.48 | 77922.48 | 0 | 386 | 0 | 75 | 0 |
OpenSMT | 0 | 6927 | 115794.58 | 115794.58 | 0 | 386 | 0 | 107 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Unsolved | Abstained | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|
Yices2 | 0 | 3324 | 54.84 | 54.84 | 0 | 294 | 92 | 0 | 0 |
OpenSMT | 0 | 1189 | 227.81 | 227.81 | 0 | 269 | 117 | 0 | 0 |
SMTInterpol | 0 | 974 | 253.73 | 253.73 | 0 | 277 | 109 | 0 | 0 |
cvc5 | 0 | 941 | 103.74 | 103.74 | 0 | 274 | 112 | 0 | 0 |