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) |
|---|---|---|---|---|
| cvc5-cvc5-xyz | cvc5-cvc5-xyz | z3-BooledASS | Bitwuzla | Z3-Z3++ |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | cvc5-cvc5-xyz | 1.183976 | 0.063903 |
| QF_LinearIntArith | QiuQi | 1.051163 | 1.879698 |
| QF_Strings | Z3-Noodler | 1.039413 | 15.944898 |
| FPArith | Bitwuzla | 1.037205 | 2.063006 |
| QF_FPArith | Bitwuzla | 1.023438 | 2.305975 |
| QF_Equality_LinearArith | z3-BooledASS | 1.0166 | 1.071103 |
| QF_Bitvec | Bitwuzla-MachBV | 1.008078 | 1.017869 |
| Bitvec | Bitwuzla-fixed | 1.003584 | 0.994181 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 1.002823 | 0.818326 |
| Equality_MachineArith | cvc5-cvc5-xyz | 1.001266 | 0.920801 |
| Equality_LinearArith | cvc5-cvc5-xyz | 1.000402 | 1.037909 |
| Equality_NonLinearArith | cvc5 | 1.00036 | 1.009823 |
| QF_Equality | Yices2 | 1 | 4.429402 |
| QF_LinearRealArith | Yices2 | 1 | 1.565533 |
| QF_NonLinearIntArith | Z3-alpha2 | 1 | 1.540731 |
| Arith | Z3-alpha2 | 1 | 1.093971 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1 | 1.043744 |
| Equality | cvc5-cvc5-xyz | 1 | 1.010125 |
| QF_NonLinearRealArith | Z3-GEX | 1 | 0.732605 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | cvc5-cvc5-xyz | 1.183976 | 0.064322 |
| QF_LinearIntArith | QiuQi | 1.050552 | 1.824652 |
| QF_Strings | Z3-Noodler | 1.039413 | 13.888814 |
| FPArith | Bitwuzla | 1.037205 | 2.049643 |
| QF_FPArith | Bitwuzla | 1.023438 | 2.294194 |
| QF_Equality_LinearArith | z3-BooledASS | 1.016018 | 0.819345 |
| QF_Bitvec | Bitwuzla-MachBV | 1.008078 | 1.017416 |
| QF_NonLinearRealArith | Z3-GEX | 1.007392 | 1.460599 |
| Bitvec | Bitwuzla-fixed | 1.003584 | 0.994428 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 1.002823 | 0.820535 |
| Equality_MachineArith | cvc5-cvc5-xyz | 1.001266 | 0.921005 |
| Equality_LinearArith | cvc5-cvc5-xyz | 1.000402 | 1.037608 |
| Equality_NonLinearArith | cvc5 | 1.00036 | 1.009679 |
| QF_Equality | Yices2 | 1 | 3.007763 |
| QF_LinearRealArith | Yices2 | 1 | 1.563135 |
| QF_NonLinearIntArith | Z3-alpha2 | 1 | 1.547993 |
| Arith | Z3-alpha2 | 1 | 1.058342 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1 | 1.023936 |
| Equality | cvc5-cvc5-xyz | 1 | 1.010122 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_NonLinearArith | z3-BooledASS | 1.229592 | 77.596473 |
| Equality_LinearArith | z3-BooledASS | 1.126027 | 18.657121 |
| FPArith | Bitwuzla | 1.073852 | 3.02557 |
| QF_Equality_NonLinearArith | Yices2 | 1.054795 | 1.916885 |
| QF_Strings | Z3-Noodler | 1.043501 | 18.510557 |
| QF_LinearIntArith | QiuQi | 1.038286 | 0.812573 |
| QF_NonLinearIntArith | Z3-Z3++ | 1.033587 | 1.287603 |
| QF_Equality_LinearArith | SMTInterpol | 1.019447 | 1.07373 |
| QF_NonLinearRealArith | Z3-GEX | 1.012658 | 1.993515 |
| QF_FPArith | Bitwuzla | 1.006981 | 1.533175 |
| QF_Bitvec | Bitwuzla-MachBV | 1.003273 | 1.435931 |
| QF_Equality_Bitvec | Bitwuzla | 1 | 1.301946 |
| QF_Equality | Yices2 | 1 | 1.178847 |
| QF_LinearRealArith | OpenSMT | 1 | 1.082559 |
| Equality_MachineArith | Bitwuzla | 1 | 1.062883 |
| Arith | Z3-alpha2 | 1 | 1.05993 |
| QF_Datatypes | cvc5-cvc5-xyz | 1 | 1.027352 |
| Bitvec | Bitwuzla | 1 | 1.006779 |
| Equality | cvc5-cvc5-xyz | 1 | 1.0002 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_FPArith | Bitwuzla | 1.034689 | 2.752453 |
| QF_Strings | Z3-Noodler | 1.034361 | 4.909074 |
| QF_LinearIntArith | QiuQi | 1.032357 | 1.720482 |
| QF_Datatypes | Z3-Z3++ | 1.018116 | 10.400674 |
| QF_Equality_LinearArith | z3-BooledASS | 1.012658 | 1.734757 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 1.00765 | 0.890886 |
| FPArith | Bitwuzla | 1.006645 | 1.182464 |
| QF_Bitvec | Bitwuzla-MachBV | 1.006334 | 1.01015 |
| Arith | Z3-GEX | 1.004405 | 0.821977 |
| QF_NonLinearIntArith | Z3-alpha2 | 1.003619 | 1.05437 |
| QF_NonLinearRealArith | Z3-GEX | 1.00211 | 1.104892 |
| Equality_LinearArith | cvc5-cvc5-xyz | 1.000434 | 1.030705 |
| Equality_MachineArith | cvc5-cvc5-xyz | 1.000395 | 0.884648 |
| Equality_NonLinearArith | cvc5 | 1.000387 | 1.011054 |
| QF_Equality | Yices2 | 1 | 4.185358 |
| QF_LinearRealArith | Yices2 | 1 | 1.420376 |
| Equality | cvc5-cvc5-xyz | 1 | 1.083249 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1 | 1.039641 |
| Bitvec | cvc5 | 1 | 1.000005 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | Z3-Z3++ | 2.325758 | 0.523158 |
| QF_FPArith | Bitwuzla | 1.124792 | 1.984946 |
| QF_Strings | Z3-Noodler | 1.12461 | 2.720238 |
| QF_LinearIntArith | Yices2 | 1.070946 | 2.056885 |
| Equality_NonLinearArith | z3-BooledASS | 1.052254 | 1.728114 |
| QF_LinearRealArith | Yices2 | 1.046472 | 1.372872 |
| QF_NonLinearRealArith | Z3-GEX | 1.028736 | 1.577852 |
| FPArith | Bitwuzla | 1.027911 | 1.227041 |
| QF_NonLinearIntArith | Z3-GEX | 1.019515 | 1.216375 |
| QF_Equality_LinearArith | z3-BooledASS | 1.019242 | 2.138602 |
| Equality | cvc5-cvc5-xyz | 1.007916 | 0.943609 |
| Equality_MachineArith | cvc5 | 1.007471 | 1.013745 |
| QF_Bitvec | Bitwuzla-MachBV | 1.006706 | 0.877601 |
| Bitvec | Bitwuzla-fixed | 1.005545 | 0.962003 |
| QF_Equality | Yices2 | 1.003571 | 1.7637 |
| Arith | Z3-GEX | 1.002924 | 3.360913 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1.002381 | 1.231856 |
| QF_Equality_Bitvec | Bitwuzla | 1 | 1.144068 |
| Equality_LinearArith | cvc5 | 1 | 1.015213 |