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 (27.384714) | cvc5 (27.384714) | — | cvc5 (27.384714) | cvc5 (16.674862) |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.575957 |
| Equality_LinearArith | cvc5 | 4.722485 |
| QF_LinearRealArith | OpenSMT | 4.458065 |
| QF_NonLinearRealArith | Yices2 | 4.452778 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.183382 |
| QF_LinearRealArith | Yices2 | 4.102475 |
| QF_Bitvec | Bitwuzla | 3.902645 |
| QF_Equality_NonLinearArith | cvc5 | 3.888269 |
| QF_LinearRealArith | cvc5 | 3.168337 |
| QF_Equality_LinearArith | Yices2 | 2.847879 |
| QF_Bitvec | Yices2 | 2.702219 |
| QF_Equality_NonLinearArith | SMTInterpol | 2.651546 |
| QF_LinearIntArith | Yices2 | 2.44221 |
| QF_NonLinearIntArith | Yices2 | 2.125728 |
| Equality_MachineArith | cvc5 | 2.027032 |
| QF_Equality_NonLinearArith | Yices2 | 2.016195 |
| QF_LinearIntArith | SMTInterpol | 1.992663 |
| QF_Equality_Bitvec | Bitwuzla | 1.980202 |
| QF_Equality | Yices2 | 1.9333 |
| Equality | SMTInterpol | 1.857655 |
| Equality_LinearArith | SMTInterpol | 1.803076 |
| QF_NonLinearIntArith | cvc5 | 1.736503 |
| QF_Equality_Bitvec | Yices2 | 1.669337 |
| QF_Equality | SMTInterpol | 1.39078 |
| QF_Equality_Bitvec | SMTInterpol | 1.333546 |
| QF_Equality | cvc5 | 1.27828 |
| Equality_MachineArith | SMTInterpol | 1.237129 |
| QF_Bitvec | cvc5 | 1.035971 |
| QF_LinearIntArith | cvc5 | 0.912855 |
| FPArith | Bitwuzla | 0.790855 |
| QF_FPArith | Bitwuzla | 0.776961 |
| QF_LinearRealArith | SMTInterpol | 0.756944 |
| QF_FPArith | cvc5 | 0.730047 |
| FPArith | cvc5 | 0.730044 |
| Equality_NonLinearArith | cvc5 | 0.549281 |
| QF_Datatypes | cvc5 | 0.369597 |
| QF_Bitvec | SMTInterpol | 0.339973 |
| QF_Equality_Bitvec | cvc5 | 0.325368 |
| Arith | cvc5 | 0.147619 |
| QF_Equality_LinearArith | cvc5 | 0.141041 |
| Equality_NonLinearArith | SMTInterpol | 0.12738 |
| QF_Equality_LinearArith | SMTInterpol | 0.068812 |
| QF_NonLinearRealArith | SMTInterpol | 0.037642 |
| QF_NonLinearRealArith | cvc5 | 0.026467 |
| Bitvec | cvc5 | 0.019563 |
| QF_Datatypes | SMTInterpol | 0.004414 |
| Bitvec | Bitwuzla | 0.001724 |
| QF_NonLinearIntArith | SMTInterpol | 0.000453 |
| Arith | SMTInterpol | 0.000102 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| Equality_MachineArith | Bitwuzla | 0 |
| Bitvec | SMTInterpol | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.169867 |
| QF_Equality | OpenSMT (min-ucore) | -11.490987 |
| QF_Equality | OpenSMT | -11.490987 |
| QF_Equality_LinearArith | OpenSMT | -12.268565 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | -12.268565 |
| Equality_LinearArith | UltimateEliminator+MathSAT | -12.655907 |
| QF_LinearIntArith | OpenSMT | -13.551086 |
| QF_LinearIntArith | OpenSMT (min-ucore) | -13.551086 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.575957 |
| Equality_LinearArith | cvc5 | 4.722485 |
| QF_LinearRealArith | OpenSMT | 4.458065 |
| QF_NonLinearRealArith | Yices2 | 4.452778 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.183382 |
| QF_LinearRealArith | Yices2 | 4.102475 |
| QF_Bitvec | Bitwuzla | 3.902645 |
| QF_Equality_NonLinearArith | cvc5 | 3.888269 |
| QF_LinearRealArith | cvc5 | 3.168337 |
| QF_Equality_LinearArith | Yices2 | 2.847879 |
| QF_Bitvec | Yices2 | 2.702219 |
| QF_Equality_NonLinearArith | SMTInterpol | 2.651546 |
| QF_LinearIntArith | Yices2 | 2.44221 |
| QF_NonLinearIntArith | Yices2 | 2.125728 |
| Equality_MachineArith | cvc5 | 2.027032 |
| QF_Equality_NonLinearArith | Yices2 | 2.016195 |
| QF_LinearIntArith | SMTInterpol | 1.992663 |
| QF_Equality_Bitvec | Bitwuzla | 1.980202 |
| QF_Equality | Yices2 | 1.9333 |
| Equality | SMTInterpol | 1.860678 |
| Equality_LinearArith | SMTInterpol | 1.80644 |
| QF_NonLinearIntArith | cvc5 | 1.736503 |
| QF_Equality_Bitvec | Yices2 | 1.669337 |
| QF_Equality | SMTInterpol | 1.39078 |
| QF_Equality_Bitvec | SMTInterpol | 1.333546 |
| QF_Equality | cvc5 | 1.27828 |
| Equality_MachineArith | SMTInterpol | 1.237129 |
| QF_Bitvec | cvc5 | 1.035971 |
| QF_LinearIntArith | cvc5 | 0.912855 |
| FPArith | Bitwuzla | 0.790855 |
| QF_FPArith | Bitwuzla | 0.776961 |
| QF_LinearRealArith | SMTInterpol | 0.760784 |
| QF_FPArith | cvc5 | 0.730047 |
| FPArith | cvc5 | 0.730044 |
| Equality_NonLinearArith | cvc5 | 0.549281 |
| QF_Datatypes | cvc5 | 0.369597 |
| QF_Bitvec | SMTInterpol | 0.341689 |
| QF_Equality_Bitvec | cvc5 | 0.325368 |
| Arith | cvc5 | 0.147619 |
| QF_Equality_LinearArith | cvc5 | 0.141041 |
| Equality_NonLinearArith | SMTInterpol | 0.12738 |
| QF_Equality_LinearArith | SMTInterpol | 0.068812 |
| QF_NonLinearRealArith | SMTInterpol | 0.037642 |
| QF_NonLinearRealArith | cvc5 | 0.026467 |
| Bitvec | cvc5 | 0.019563 |
| QF_Datatypes | SMTInterpol | 0.004414 |
| Bitvec | Bitwuzla | 0.001724 |
| QF_NonLinearIntArith | SMTInterpol | 0.000453 |
| Arith | SMTInterpol | 0.000102 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| Equality_MachineArith | Bitwuzla | 0 |
| Bitvec | SMTInterpol | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.169867 |
| QF_Equality | OpenSMT (min-ucore) | -11.490987 |
| QF_Equality | OpenSMT | -11.490987 |
| QF_Equality_LinearArith | OpenSMT | -12.268565 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | -12.268565 |
| Equality_LinearArith | UltimateEliminator+MathSAT | -12.655907 |
| QF_LinearIntArith | OpenSMT | -13.551086 |
| QF_LinearIntArith | OpenSMT (min-ucore) | -13.551086 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.575957 |
| Equality_LinearArith | cvc5 | 4.722485 |
| QF_LinearRealArith | OpenSMT | 4.458065 |
| QF_NonLinearRealArith | Yices2 | 4.452778 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.183382 |
| QF_LinearRealArith | Yices2 | 4.102475 |
| QF_Bitvec | Bitwuzla | 3.902645 |
| QF_Equality_NonLinearArith | cvc5 | 3.888269 |
| QF_LinearRealArith | cvc5 | 3.168337 |
| QF_Equality_LinearArith | Yices2 | 2.847879 |
| QF_Bitvec | Yices2 | 2.702219 |
| QF_Equality_NonLinearArith | SMTInterpol | 2.651546 |
| QF_LinearIntArith | Yices2 | 2.44221 |
| QF_NonLinearIntArith | Yices2 | 2.125728 |
| Equality_MachineArith | cvc5 | 2.027032 |
| QF_Equality_NonLinearArith | Yices2 | 2.016195 |
| QF_LinearIntArith | SMTInterpol | 1.992663 |
| QF_Equality_Bitvec | Bitwuzla | 1.980202 |
| QF_Equality | Yices2 | 1.9333 |
| Equality | SMTInterpol | 1.860678 |
| Equality_LinearArith | SMTInterpol | 1.80644 |
| QF_NonLinearIntArith | cvc5 | 1.736503 |
| QF_Equality_Bitvec | Yices2 | 1.669337 |
| QF_Equality | SMTInterpol | 1.39078 |
| QF_Equality_Bitvec | SMTInterpol | 1.333546 |
| QF_Equality | cvc5 | 1.27828 |
| Equality_MachineArith | SMTInterpol | 1.237129 |
| QF_Bitvec | cvc5 | 1.035971 |
| QF_LinearIntArith | cvc5 | 0.912855 |
| FPArith | Bitwuzla | 0.790855 |
| QF_FPArith | Bitwuzla | 0.776961 |
| QF_LinearRealArith | SMTInterpol | 0.760784 |
| QF_FPArith | cvc5 | 0.730047 |
| FPArith | cvc5 | 0.730044 |
| Equality_NonLinearArith | cvc5 | 0.549281 |
| QF_Datatypes | cvc5 | 0.369597 |
| QF_Bitvec | SMTInterpol | 0.341689 |
| QF_Equality_Bitvec | cvc5 | 0.325368 |
| Arith | cvc5 | 0.147619 |
| QF_Equality_LinearArith | cvc5 | 0.141041 |
| Equality_NonLinearArith | SMTInterpol | 0.12738 |
| QF_Equality_LinearArith | SMTInterpol | 0.068812 |
| QF_NonLinearRealArith | SMTInterpol | 0.037642 |
| QF_NonLinearRealArith | cvc5 | 0.026467 |
| Bitvec | cvc5 | 0.019563 |
| QF_Datatypes | SMTInterpol | 0.004414 |
| Bitvec | Bitwuzla | 0.001724 |
| QF_NonLinearIntArith | SMTInterpol | 0.000453 |
| Arith | SMTInterpol | 0.000102 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| Equality_MachineArith | Bitwuzla | 0 |
| Bitvec | SMTInterpol | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.169867 |
| QF_Equality | OpenSMT (min-ucore) | -11.490987 |
| QF_Equality | OpenSMT | -11.490987 |
| QF_Equality_LinearArith | OpenSMT | -12.268565 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | -12.268565 |
| Equality_LinearArith | UltimateEliminator+MathSAT | -12.655907 |
| QF_LinearIntArith | OpenSMT | -13.551086 |
| QF_LinearIntArith | OpenSMT (min-ucore) | -13.551086 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.017413 |
| Equality_LinearArith | cvc5 | 4.295946 |
| QF_Bitvec | Bitwuzla | 2.647555 |
| QF_Bitvec | Yices2 | 2.593216 |
| QF_LinearRealArith | Yices2 | 2.136636 |
| QF_LinearIntArith | Yices2 | 2.069325 |
| QF_NonLinearIntArith | Yices2 | 1.939141 |
| QF_Equality_NonLinearArith | Yices2 | 1.907774 |
| QF_LinearRealArith | OpenSMT | 1.838936 |
| QF_Equality_NonLinearArith | SMTInterpol | 1.7893 |
| Equality_MachineArith | cvc5 | 1.784752 |
| QF_Equality | Yices2 | 1.748876 |
| Equality_LinearArith | SMTInterpol | 1.682844 |
| QF_Equality_Bitvec | Bitwuzla | 1.463705 |
| Equality | SMTInterpol | 1.383537 |
| QF_NonLinearIntArith | cvc5 | 1.204346 |
| QF_Equality | SMTInterpol | 1.191736 |
| QF_Equality_Bitvec | Yices2 | 1.177553 |
| QF_Equality | cvc5 | 1.123166 |
| QF_Equality_Bitvec | SMTInterpol | 1.050389 |
| Equality_MachineArith | SMTInterpol | 1.030475 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 0.987252 |
| FPArith | Bitwuzla | 0.790855 |
| FPArith | cvc5 | 0.730044 |
| QF_FPArith | Bitwuzla | 0.724263 |
| QF_FPArith | cvc5 | 0.665714 |
| QF_LinearIntArith | cvc5 | 0.526957 |
| QF_NonLinearRealArith | Yices2 | 0.479749 |
| QF_LinearIntArith | SMTInterpol | 0.444536 |
| QF_Equality_NonLinearArith | cvc5 | 0.375218 |
| Equality_NonLinearArith | cvc5 | 0.27829 |
| QF_LinearRealArith | cvc5 | 0.235488 |
| QF_Bitvec | cvc5 | 0.19226 |
| QF_Equality_Bitvec | cvc5 | 0.175485 |
| Equality_NonLinearArith | SMTInterpol | 0.109727 |
| QF_Equality_LinearArith | Yices2 | 0.074576 |
| QF_Bitvec | SMTInterpol | 0.059579 |
| QF_LinearRealArith | SMTInterpol | 0.057633 |
| QF_NonLinearRealArith | SMTInterpol | 0.037642 |
| Arith | cvc5 | 0.031053 |
| QF_NonLinearRealArith | cvc5 | 0.02392 |
| Bitvec | cvc5 | 0.010107 |
| QF_Equality_LinearArith | cvc5 | 0.004705 |
| Bitvec | Bitwuzla | 0.001724 |
| QF_Equality_LinearArith | SMTInterpol | 0.000659 |
| QF_NonLinearIntArith | SMTInterpol | 0.000439 |
| Arith | SMTInterpol | 0.000102 |
| QF_Datatypes | SMTInterpol | 1e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| Equality_MachineArith | Bitwuzla | 0 |
| QF_Datatypes | cvc5 | 0 |
| Bitvec | SMTInterpol | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.169867 |
| QF_Equality | OpenSMT (min-ucore) | -11.490987 |
| QF_Equality | OpenSMT | -11.490987 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | -12.268565 |
| QF_Equality_LinearArith | OpenSMT | -12.268565 |
| Equality_LinearArith | UltimateEliminator+MathSAT | -12.655907 |
| QF_LinearIntArith | OpenSMT (min-ucore) | -13.551086 |
| QF_LinearIntArith | OpenSMT | -13.551086 |