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) |
|---|---|---|---|---|
| - | OpenSMT-SMTS | OpenSMT-SMTS | Yices2 | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_LinearRealArith | OpenSMT-SMTS | 4.6 | 0.432435 |
| QF_NonLinearRealArith | Yices2 | 3.25 | 0.010142 |
| QF_Equality_LinearArith | z3-parallel | 2.714286 | 0.458005 |
| QF_Bitvec | Bitwuzllob | 1.736842 | 0.969306 |
| QF_LinearIntArith | OpenSMT-SMTS | 1.08 | 2.830616 |
| QF_NonLinearIntArith | Yices2 | 1 | 1.596161 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_LinearRealArith | OpenSMT-SMTS | 12 | 0.000176 |
| QF_Equality_LinearArith | z3-parallel | 3.5 | 0.345364 |
| QF_LinearIntArith | OpenSMT-SMTS | 2 | 1.009194 |
| QF_NonLinearRealArith | Yices2 | 1.5 | 3.648956 |
| QF_Bitvec | Bitwuzllob | 1.375 | 1.017005 |
| QF_NonLinearIntArith | Yices2 | 1.1 | 1.304519 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_NonLinearRealArith | Yices2 | 8 | 0.00033 |
| QF_LinearRealArith | OpenSMT-SMTS | 2.4 | 1.629498 |
| QF_Bitvec | Bitwuzllob | 1.916667 | 0.937162 |
| QF_Equality_LinearArith | z3-parallel | 1.5 | 0.662419 |
| QF_LinearIntArith | z3-parallel | 1.444444 | 0.153449 |
| QF_NonLinearIntArith | z3-parallel | 1.2 | 0.523876 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_NonLinearRealArith | Yices2 | 2.25 | 1.6063 |
| QF_NonLinearIntArith | Yices2 | 1.4 | 0.811583 |
| QF_LinearIntArith | OpenSMT-SMTS | 1.333333 | 0.584889 |