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 | Z3-Noodler-Mocha | cvc5 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_LinearArith | cvc5 | 0.008899 | 0.024368 |
| Equality_NonLinearArith | cvc5 | 0.007342 | 0.001827 |
| Equality_MachineArith | cvc5 | 0.004893 | -0.018558 |
| QF_Strings | Z3-Noodler-Mocha | 0.003231 | 0.136272 |
| Equality | cvc5 | 0.001958 | -0.007166 |
| Equality_MachineArith | Bitwuzla | 0.00107 | 0.000391 |
| QF_NonLinearIntArith | z3siri | 0.000982 | -0.002856 |
| QF_NonLinearIntArith | Z3-alpha | 0.000931 | -0.002136 |
| QF_NonLinearIntArith | Yices2 | 0.000555 | 0.025284 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000406 | 0.000401 |
| Equality_MachineArith | SMTInterpol | 0.000316 | 0.001883 |
| Equality_LinearArith | iProver v3.9.3 | 0.000308 | 0.001316 |
| QF_NonLinearIntArith | cvc5 | 0.000307 | -0.009183 |
| QF_Equality_Bitvec | cvc5 | 0.0003 | -0.01066 |
| QF_Bitvec | Yices2 | 0.000282 | 0.011208 |
| Bitvec | cvc5 | 0.000277 | -0.002451 |
| QF_Equality_Bitvec | SMTInterpol | 0.000273 | 0.00398 |
| FPArith | Bitwuzla | 0.00027 | 0.001647 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.00027 | -0.001329 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_LinearArith | cvc5 | 0.007527 | 0.024634 |
| Equality_NonLinearArith | cvc5 | 0.006011 | 0.008065 |
| Equality_MachineArith | cvc5 | 0.004893 | -0.024345 |
| QF_Strings | Z3-Noodler-Mocha | 0.003231 | 0.063843 |
| Equality | cvc5 | 0.001784 | -0.009147 |
| QF_NonLinearIntArith | Z3-alpha | 0.001116 | 0.011004 |
| Equality_MachineArith | Bitwuzla | 0.00107 | 0.000375 |
| QF_NonLinearIntArith | z3siri | 0.000946 | -0.006788 |
| QF_NonLinearIntArith | Yices2 | 0.000545 | 0.020941 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.000418 | -0.000524 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000405 | 0.000409 |
| Equality_LinearArith | iProver v3.9.3 | 0.000394 | 0.000214 |
| Equality_MachineArith | SMTInterpol | 0.000316 | 0.001982 |
| QF_Equality_Bitvec | cvc5 | 0.0003 | -0.011816 |
| QF_Bitvec | Yices2 | 0.000282 | 0.010929 |
| Bitvec | cvc5 | 0.000277 | -0.002437 |
| QF_Equality_Bitvec | SMTInterpol | 0.000273 | 0.00775 |
| FPArith | Bitwuzla | 0.00027 | 0.001629 |
| QF_NonLinearIntArith | cvc5 | 0.000264 | -0.012915 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_LinearArith | cvc5 | 0.031831 | -6.952655 |
| Equality_NonLinearArith | cvc5 | 0.008722 | -0.05279 |
| Equality_MachineArith | cvc5 | 0.007711 | -0.163741 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.005299 | -0.000178 |
| Equality | cvc5 | 0.002924 | -0.107743 |
| Equality_MachineArith | Bitwuzla | 0.002326 | -0.000213 |
| QF_NonLinearIntArith | Z3-alpha | 0.001528 | 0.017928 |
| FPArith | Bitwuzla | 0.000548 | 0.002635 |
| QF_NonLinearIntArith | Yices2 | 0.000462 | 0.023635 |
| QF_Equality_Bitvec | cvc5 | 0.000406 | -0.029073 |
| QF_Bitvec | Yices2 | 0.000401 | 0.013518 |
| QF_NonLinearIntArith | cvc5 | 0.000385 | -0.021993 |
| QF_Equality_LinearArith | SMTInterpol | 0.00029 | 0.000514 |
| Equality_MachineArith | SMTInterpol | 0.000279 | -2e-06 |
| QF_Equality_NonLinearArith | Yices2 | 0.000258 | 0.000909 |
| QF_Bitvec | Bitwuzla | 0.000241 | 0.007282 |
| QF_LinearIntArith | OpenSMT | 0.000232 | 0.000792 |
| Arith | YicesQS | 0.000181 | 0.009289 |
| Bitvec | cvc5 | 0.00017 | -0.002375 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Strings | Z3-Noodler-Mocha | 0.009162 | 0.181973 |
| Equality_NonLinearArith | cvc5 | 0.005696 | 0.009231 |
| Equality_LinearArith | cvc5 | 0.005559 | 0.029079 |
| Equality_MachineArith | cvc5 | 0.003982 | -0.007288 |
| QF_NonLinearIntArith | z3siri | 0.002634 | -0.036338 |
| Equality | cvc5 | 0.001318 | 0.002436 |
| QF_Equality_Bitvec | SMTInterpol | 0.000782 | 0.010791 |
| QF_NonLinearIntArith | Yices2 | 0.000709 | 0.015437 |
| Equality_MachineArith | Bitwuzla | 0.000665 | 0.000919 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.000466 | -0.00058 |
| Equality_LinearArith | iProver v3.9.3 | 0.000426 | 0.000322 |
| Equality_MachineArith | SMTInterpol | 0.000327 | 0.00349 |
| Bitvec | cvc5 | 0.000312 | -0.002466 |
| QF_NonLinearIntArith | Z3-alpha | 0.000304 | -0.005745 |
| QF_LinearIntArith | cvc5 | 0.000289 | 0.010459 |
| QF_FPArith | Bitwuzla | 0.000274 | 0.005922 |
| Arith | YicesQS | 0.000249 | 0.009961 |
| QF_Bitvec | Bitwuzla-MachBV | 0.000248 | 0.02524 |
| QF_Equality_Bitvec | Bitwuzla | 0.000227 | 0.016445 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_LinearArith | cvc5 | 0.011868 | 0.025679 |
| Equality_NonLinearArith | cvc5 | 0.008058 | 0.009695 |
| QF_LinearIntArith | Yices2 | 0.004913 | 0.026228 |
| Equality_MachineArith | cvc5 | 0.004055 | 0.004711 |
| QF_Strings | Z3-Noodler-Mocha | 0.003466 | 0.069201 |
| QF_NonLinearIntArith | Yices2 | 0.002637 | 0.018382 |
| Equality | cvc5 | 0.00176 | 0.00256 |
| QF_NonLinearIntArith | Z3-alpha | 0.0013 | 0.007156 |
| Equality_MachineArith | Bitwuzla | 0.001205 | -0.003526 |
| Equality | iProver v3.9.3 | 0.001062 | -0.00318 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.000858 | -0.003647 |
| QF_Bitvec | Yices2 | 0.000772 | 0.030449 |
| Equality_MachineArith | SMTInterpol | 0.000765 | -0.001486 |
| QF_Equality_Bitvec | Bitwuzla | 0.000689 | 0.000266 |
| Equality_LinearArith | iProver v3.9.3 | 0.000586 | -0.003413 |
| QF_FPArith | Bitwuzla | 0.000529 | 0.003022 |
| Arith | YicesQS | 0.000506 | 0.006592 |
| QF_NonLinearIntArith | z3siri | 0.000476 | 0.004767 |
| QF_Equality_NonLinearArith | Yices2 | 0.000448 | -0.000458 |