The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_Equality_LinearArith division in the Unsat Core Track. Chart
Results were generated on 2025-08-11
Benchmarks: 591
Time Limit: 1200 seconds
Memory Limit: 30720 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | - | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 928242 | 25957.87 | 26026.60 | 531 | 531 | 36 | 24 | 35 | 0 |
| cvc5 | 0 | 206573 | 5898.73 | 5962.50 | 496 | 496 | 95 | 0 | 95 | 0 |
| SMTInterpol | 0 | 144289 | 3368.07 | 2274.73 | 488 | 488 | 103 | 0 | 94 | 0 |
| OpenSMT (min-ucore) | 18 | 24873 | 10999.44 | 11051.64 | 412 | 412 | 155 | 24 | 134 | 0 |
| OpenSMT | 20 | 722868 | 23490.02 | 23556.37 | 501 | 501 | 66 | 24 | 43 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 928242 | 25957.87 | 26026.60 | 531 | 531 | 36 | 24 | 35 | 0 |
| cvc5 | 0 | 206573 | 5898.73 | 5962.50 | 496 | 496 | 95 | 0 | 95 | 0 |
| SMTInterpol | 0 | 144289 | 3368.07 | 2274.73 | 488 | 488 | 103 | 0 | 94 | 0 |
| OpenSMT (min-ucore) | 18 | 24873 | 10999.44 | 11051.64 | 412 | 412 | 155 | 24 | 134 | 0 |
| OpenSMT | 20 | 722868 | 23490.02 | 23556.37 | 501 | 501 | 66 | 24 | 43 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 928242 | 25957.87 | 26026.60 | 531 | 531 | 36 | 24 | 35 | 0 |
| cvc5 | 0 | 206573 | 5898.73 | 5962.50 | 496 | 496 | 95 | 0 | 95 | 0 |
| SMTInterpol | 0 | 144289 | 3368.07 | 2274.73 | 488 | 488 | 103 | 0 | 94 | 0 |
| OpenSMT (min-ucore) | 18 | 24873 | 10999.44 | 11051.64 | 412 | 412 | 155 | 24 | 134 | 0 |
| OpenSMT | 20 | 722868 | 23490.02 | 23556.37 | 501 | 501 | 66 | 24 | 43 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 150210 | 145.91 | 203.41 | 468 | 468 | 0 | 123 | 0 | 0 |
| cvc5 | 0 | 37728 | 214.01 | 274.85 | 482 | 482 | 0 | 109 | 0 | 0 |
| SMTInterpol | 0 | 14116 | 1009.91 | 504.77 | 475 | 475 | 0 | 116 | 0 | 0 |
| OpenSMT (min-ucore) | 17 | 2142 | 387.55 | 430.94 | 354 | 354 | 20 | 217 | 0 | 0 |
| OpenSMT | 19 | 4104 | 137.71 | 192.33 | 437 | 437 | 22 | 132 | 0 | 0 |