The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2025-08-11
| Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|
| cvc5 | - | - | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_NonLinearArith | cvc5 | 0.02336 | 0.027846 |
| QF_Equality_LinearArith | Yices2 | 0.018803 | 0.059723 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.00498 | 0.014741 |
| Equality_NonLinearArith | SMTInterpol | 0.004532 | -0.000718 |
| QF_Equality_LinearArith | SMTInterpol | 0.002523 | 0.039366 |
| QF_Equality_Bitvec | Bitwuzla | 0.001372 | 0.050923 |
| QF_Bitvec | Yices2 | 0.000849 | 0.015025 |
| Equality_LinearArith | cvc5 | 0.000811 | 0.022805 |
| QF_Bitvec | Bitwuzla | 0.000457 | 0.015155 |
| FPArith | Bitwuzla | 0.000214 | 3.9e-05 |
| Equality_MachineArith | Bitwuzla | 0.00014 | 0.000167 |
| QF_Equality_Bitvec_Arith | Yices2 | 0.000108 | 0.038221 |
| Bitvec | Bitwuzla | 8.1e-05 | 0.000461 |
| QF_Equality_Bitvec | Yices2 | 7.9e-05 | 0.101281 |
| QF_LinearIntArith | Yices2 | 7.7e-05 | 0.001928 |
| QF_LinearRealArith | OpenSMT | 6.7e-05 | 0.000227 |
| QF_LinearRealArith | Yices2 | 6.2e-05 | 0 |
| QF_Equality_LinearArith | cvc5 | 3e-05 | 0.00345 |
| Bitvec | cvc5 | 1.8e-05 | 0.000172 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Equality_LinearArith | Yices2 | 0.117499 | 0.051167 |
| Equality_NonLinearArith | cvc5 | 0.02034 | -0.139117 |
| QF_Equality_Bitvec | SMTInterpol | 0.015824 | 0.001407 |
| QF_Equality_LinearArith | SMTInterpol | 0.007551 | -0.008782 |
| Equality_NonLinearArith | SMTInterpol | 0.006359 | 0.001096 |
| QF_Equality_NonLinearArith | cvc5 | 0.005907 | 0.000905 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.005199 | 0.009224 |
| QF_LinearIntArith | Yices2 | 0.005009 | -0.004454 |
| QF_Bitvec | SMTInterpol | 0.004193 | -4.2e-05 |
| QF_Equality_Bitvec | Bitwuzla | 0.003526 | 0.014562 |
| QF_NonLinearIntArith | Yices2 | 0.003493 | -0.001413 |
| QF_Equality_Bitvec_Arith | Yices2 | 0.003309 | 0.024613 |
| QF_Bitvec | Yices2 | 0.003043 | 0.007919 |
| QF_Equality_Bitvec | Yices2 | 0.002933 | 0.050564 |
| Equality_LinearArith | SMTInterpol | 0.001328 | 0.001774 |
| Equality_LinearArith | cvc5 | 0.001304 | -0.027287 |
| QF_NonLinearIntArith | SMTInterpol | 0.001256 | -0.005787 |
| QF_NonLinearIntArith | Z3-Inc-Z3++ | 0.000893 | 0 |
| QF_Equality_Bitvec | cvc5 | 0.00048 | -0.00118 |