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) |
|---|---|---|---|
| Bitwuzla | - | - | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_MachineArith | Bitwuzla | 2.771673 | 0.193079 |
| Equality | cvc5 | 2.078357 | 4.366691 |
| Equality_NonLinearArith | cvc5 | 1.675505 | 4.445631 |
| FPArith | Bitwuzla | 1.644556 | 0.09317 |
| QF_Equality_NonLinearArith | SMTInterpol | 1.188197 | 10.602028 |
| QF_FPArith | Bitwuzla | 1.107071 | 21.964855 |
| Arith | cvc5 | 1.084789 | 14.738061 |
| QF_Equality_LinearArith | SMTInterpol | 1.045379 | 1.165492 |
| Equality_LinearArith | cvc5 | 1.033467 | 8.555007 |
| Bitvec | cvc5 | 1.022046 | 0.234721 |
| QF_LinearRealArith | OpenSMT | 1.015658 | 1.453802 |
| QF_LinearIntArith | Yices2 | 1.015627 | 1.639626 |
| QF_Equality_Bitvec | Bitwuzla | 1.010091 | 0.503223 |
| QF_NonLinearIntArith | Z3-Inc-Z3++ | 1.006183 | 0.811674 |
| QF_Equality_Bitvec_Arith | Yices2 | 1.004592 | 4.779713 |
| QF_Bitvec | Yices2 | 1.00192 | 0.851529 |
| QF_Equality | Yices2 | 1 | 4.199948 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_LinearIntArith | Yices2 | 480.536009 | 0.761368 |
| Equality | cvc5 | 2.796666 | 0.193835 |
| QF_NonLinearIntArith | Yices2 | 2.307692 | 1.864166 |
| Equality_NonLinearArith | cvc5 | 2.110765 | 0.204826 |
| QF_Equality_LinearArith | Yices2 | 2.04854 | 2.731351 |
| QF_FPArith | Bitwuzla | 1.589484 | 3.30433 |
| FPArith | Bitwuzla | 1.309762 | 0.35593 |
| Bitvec | cvc5 | 1.189755 | 0.610055 |
| Arith | SMTInterpol | 1.139203 | 0.623148 |
| Equality_MachineArith | cvc5 | 1.102288 | 1.462209 |
| QF_Equality_Bitvec_Arith | Yices2 | 1.073292 | 1.515629 |
| QF_Bitvec | Yices2 | 1.02541 | 1.11554 |
| QF_Equality_Bitvec | Yices2 | 1.022205 | 1.367319 |
| QF_Equality_NonLinearArith | cvc5 | 1.004794 | 0.57519 |
| Equality_LinearArith | SMTInterpol | 1.001047 | 2.439115 |
| QF_Equality | Yices2 | 1 | 4.199948 |