The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2026-07-25
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| — | Bitwuzllob (0.649847) | OpenSMT-SMTS (0.169397) | Bitwuzllob (0.307154) | Yices2 (0.067959) |
| Division | Solver | Contribution |
|---|---|---|
| QF_Bitvec | Bitwuzllob | 0.649847 |
| QF_Bitvec | Bitwuzla-BV_Parti | 0.205616 |
| QF_LinearRealArith | OpenSMT-SMTS | 0.191811 |
| QF_NonLinearIntArith | z3-parallel | 0.133199 |
| QF_NonLinearIntArith | Yices2 | 0.133199 |
| QF_LinearRealArith | OpenSMT-SMTS-base | 0.128402 |
| QF_LinearIntArith | OpenSMT-SMTS | 0.128257 |
| QF_LinearIntArith | z3-parallel | 0.109284 |
| QF_Equality_LinearArith | z3-parallel | 0.10309 |
| QF_NonLinearRealArith | Yices2 | 0.097861 |
| QF_Equality_LinearArith | OpenSMT-SMTS-base | 0.045818 |
| QF_LinearIntArith | QiuQi | 0.037187 |
| QF_LinearIntArith | OpenSMT-SMTS-base | 0.022957 |
| QF_Equality_LinearArith | OpenSMT-SMTS | 0.011454 |
| QF_LinearRealArith | z3-parallel | 0.006341 |
| QF_NonLinearRealArith | z3-parallel | 0.006116 |
| Division | Solver | Contribution |
|---|---|---|
| QF_LinearIntArith | OpenSMT-SMTS | 0.118581 |
| QF_NonLinearIntArith | Yices2 | 0.067959 |
| QF_Bitvec | Bitwuzllob | 0.063462 |
| QF_NonLinearIntArith | z3-parallel | 0.055047 |
| QF_Equality_LinearArith | z3-parallel | 0.053772 |
| QF_LinearRealArith | OpenSMT-SMTS | 0.047953 |
| QF_Bitvec | Bitwuzla-BV_Parti | 0.031096 |
| QF_LinearIntArith | z3-parallel | 0.027321 |
| QF_LinearRealArith | OpenSMT-SMTS-base | 0.019419 |
| QF_LinearIntArith | OpenSMT-SMTS-base | 0.018973 |
| QF_NonLinearRealArith | Yices2 | 0.01699 |
| QF_LinearIntArith | QiuQi | 0.00683 |
| QF_NonLinearRealArith | z3-parallel | 0.006116 |
| QF_Equality_LinearArith | OpenSMT-SMTS | 0.002864 |
| QF_Equality_LinearArith | OpenSMT-SMTS-base | 0.000318 |
| QF_LinearRealArith | z3-parallel | 0 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Bitvec | Bitwuzllob | 0.307154 |
| QF_Bitvec | Bitwuzla-BV_Parti | 0.076789 |
| QF_LinearRealArith | OpenSMT-SMTS-base | 0.047953 |
| QF_LinearRealArith | OpenSMT-SMTS | 0.047953 |
| QF_Equality_LinearArith | OpenSMT-SMTS-base | 0.0385 |
| QF_NonLinearRealArith | Yices2 | 0.0333 |
| QF_LinearIntArith | z3-parallel | 0.027321 |
| QF_NonLinearIntArith | z3-parallel | 0.01699 |
| QF_LinearIntArith | QiuQi | 0.012143 |
| QF_NonLinearIntArith | Yices2 | 0.010873 |
| QF_Equality_LinearArith | z3-parallel | 0.007955 |
| QF_LinearRealArith | z3-parallel | 0.006341 |
| QF_Equality_LinearArith | OpenSMT-SMTS | 0.002864 |
| QF_LinearIntArith | OpenSMT-SMTS-base | 0.00019 |
| QF_LinearIntArith | OpenSMT-SMTS | 0.00019 |
| QF_NonLinearRealArith | z3-parallel | 0 |
| Division | Solver | Contribution |
|---|---|---|
| QF_NonLinearRealArith | Yices2 | 0.043494 |
| QF_NonLinearIntArith | Yices2 | 0.024465 |
| QF_NonLinearIntArith | z3-parallel | 0.010873 |
| QF_NonLinearRealArith | z3-parallel | 0.006116 |
| QF_LinearIntArith | OpenSMT-SMTS | 0.001708 |
| QF_LinearIntArith | QiuQi | 0.000759 |