The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2025-08-11
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_MachineArith | cvc5 | 1.917285 | 0.247241 |
| QF_Datatypes | cvc5 | 1.707692 | 0.395056 |
| Equality_NonLinearArith | cvc5 | 1.683696 | 1.46668 |
| Equality | cvc5 | 1.619452 | 0.322912 |
| Equality_LinearArith | cvc5 | 1.305197 | 2.678634 |
| QF_Equality_NonLinearArith | Yices2 | 1.180628 | 1.78793 |
| Bitvec | cvc5 | 1.074408 | 0.539141 |
| Arith | Z3-alpha | 1.066522 | 0.039414 |
| FPArith | Bitwuzla | 1.031802 | 0.942458 |
| QF_NonLinearIntArith | Z3-alpha | 1.028059 | 0.982487 |
| QF_FPArith | Bitwuzla | 1.019582 | 2.798526 |
| QF_NonLinearRealArith | Z3-alpha | 1.018902 | 1.196563 |
| QF_LinearIntArith | OpenSMT | 1.017289 | 0.280196 |
| QF_Strings | Z3-Noodler-Mocha | 1.014122 | 1.045924 |
| QF_Equality_Bitvec | Bitwuzla | 1.005953 | 2.554068 |
| QF_Bitvec | Bitwuzla-MachBV | 1.002381 | 1.028872 |
| QF_Equality_LinearArith | SMTInterpol | 1.00167 | 1.385826 |
| QF_LinearRealArith | Yices2 | 1.001289 | 1.142397 |
| QF_Equality | Yices2 | 1.000262 | 4.62082 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_MachineArith | cvc5 | 1.917285 | 0.189347 |
| QF_Datatypes | cvc5 | 1.69898 | 0.287108 |
| Equality | cvc5 | 1.501751 | 0.272888 |
| Equality_NonLinearArith | cvc5 | 1.490027 | 1.79049 |
| Equality_LinearArith | cvc5 | 1.241649 | 2.819353 |
| QF_Equality_NonLinearArith | Yices2 | 1.180628 | 1.78458 |
| Arith | Z3-alpha | 1.096168 | 0.037009 |
| Bitvec | cvc5 | 1.074408 | 0.540515 |
| QF_NonLinearIntArith | Z3-alpha | 1.041366 | 1.990752 |
| FPArith | Bitwuzla | 1.031802 | 0.942542 |
| QF_NonLinearRealArith | Z3-alpha | 1.024608 | 2.379179 |
| QF_FPArith | Bitwuzla | 1.019582 | 2.777475 |
| QF_LinearIntArith | OpenSMT | 1.017289 | 0.28169 |
| QF_Strings | Z3-Noodler-Mocha | 1.014122 | 1.036289 |
| QF_Equality_Bitvec | Bitwuzla | 1.005953 | 2.498694 |
| QF_Bitvec | Bitwuzla-MachBV | 1.002381 | 1.028429 |
| QF_Equality_LinearArith | SMTInterpol | 1.00167 | 1.873656 |
| QF_LinearRealArith | Yices2 | 1.001289 | 1.141964 |
| QF_Equality | Yices2 | 1.000262 | 3.813016 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | cvc5 | 2.93617 | 0.589223 |
| Equality_MachineArith | cvc5 | 2.75 | 0.075009 |
| Equality | cvc5 | 2.131356 | 0.028889 |
| Equality_NonLinearArith | cvc5 | 1.63908 | 0.239157 |
| Equality_LinearArith | cvc5 | 1.542705 | 0.00625 |
| QF_Equality_NonLinearArith | Yices2 | 1.26936 | 1.841259 |
| FPArith | Bitwuzla | 1.100971 | 1.722072 |
| QF_NonLinearIntArith | Z3-alpha | 1.068697 | 2.036625 |
| QF_Equality_LinearArith | SMTInterpol | 1.031977 | 1.514291 |
| QF_NonLinearRealArith | Z3-alpha | 1.027581 | 1.805178 |
| Arith | Z3-alpha | 1.022569 | 0.041534 |
| QF_FPArith | Bitwuzla | 1.010033 | 1.393649 |
| Bitvec | Bitwuzla | 1.008658 | 3.752137 |
| QF_LinearRealArith | OpenSMT | 1.007026 | 0.551153 |
| QF_LinearIntArith | Z3-alpha | 1.004768 | 2.623635 |
| QF_Equality_Bitvec | Bitwuzla | 1.000924 | 2.403491 |
| QF_Bitvec | Bitwuzla | 1.000406 | 1.121292 |
| QF_Strings | Z3-Noodler-Mocha | 1.000226 | 1.003315 |
| QF_Equality | Yices2 | 1 | 1.312704 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_MachineArith | cvc5 | 1.520393 | 0.322914 |
| Equality | cvc5 | 1.337376 | 1.713123 |
| Equality_NonLinearArith | cvc5 | 1.332225 | 2.032051 |
| QF_Datatypes | cvc5 | 1.306667 | 0.209088 |
| Equality_LinearArith | cvc5 | 1.159936 | 4.197266 |
| QF_Equality_NonLinearArith | cvc5 | 1.146667 | 0.685666 |
| Bitvec | cvc5 | 1.108067 | 0.429454 |
| Arith | Z3-alpha | 1.084112 | 1.431754 |
| QF_Strings | Z3-Noodler-Mocha | 1.0407 | 1.114476 |
| QF_FPArith | Bitwuzla | 1.025668 | 4.055108 |
| QF_LinearIntArith | OpenSMT | 1.016323 | 0.20553 |
| QF_Equality_LinearArith | OpenSMT | 1.015686 | 1.022555 |
| QF_Equality_Bitvec | Bitwuzla | 1.015603 | 2.578469 |
| QF_NonLinearIntArith | z3siri | 1.009524 | 0.528812 |
| QF_LinearRealArith | Yices2 | 1.005731 | 0.936635 |
| QF_NonLinearRealArith | Z3-alpha | 1.00495 | 3.228739 |
| QF_Bitvec | Bitwuzla-MachBV | 1.004849 | 1.172407 |
| FPArith | Bitwuzla | 1.001689 | 0.482973 |
| QF_Equality | Yices2 | 1.000455 | 4.524926 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_NonLinearArith | cvc5 | 1.885146 | 2.417995 |
| Equality_MachineArith | cvc5 | 1.643167 | 1.453804 |
| Equality_LinearArith | cvc5 | 1.446632 | 3.466322 |
| Equality | cvc5 | 1.2575 | 3.547819 |
| QF_Equality_NonLinearArith | Yices2 | 1.248252 | 0.973796 |
| QF_Datatypes | SMTInterpol | 1.145631 | 0.992546 |
| QF_FPArith | Bitwuzla | 1.141975 | 2.125353 |
| QF_LinearIntArith | Yices2 | 1.093999 | 2.166178 |
| Bitvec | YicesQS | 1.063052 | 1.367135 |
| QF_NonLinearIntArith | Z3-alpha | 1.057043 | 0.830119 |
| QF_LinearRealArith | Yices2 | 1.035994 | 1.331973 |
| Arith | Z3-alpha | 1.026831 | 0.311741 |
| QF_Equality_Bitvec | Bitwuzla | 1.026777 | 0.601514 |
| QF_NonLinearRealArith | Z3-alpha | 1.02164 | 0.593258 |
| QF_Strings | Z3-Noodler-Mocha | 1.014839 | 1.012418 |
| QF_Equality_LinearArith | SMTInterpol | 1.009445 | 0.252833 |
| FPArith | Bitwuzla | 1.008755 | 1.325511 |
| QF_Bitvec | Bitwuzla-MachBV | 1.008184 | 0.80618 |
| QF_Equality | Yices2 | 1.006324 | 2.175748 |