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) |
|---|---|---|---|---|
| SMTInterpol | SMTInterpol | SMTInterpol | - | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | SMTInterpol | 1.395137 | 1.408922 |
| QF_Equality_NonLinearArith | cvc5 | 1.251773 | 0.929269 |
| QF_ADT_BitVec | Bitwuzla | 1.095348 | 20.929064 |
| QF_NonLinearIntArith | Yices2 | 1.072645 | 36.175695 |
| QF_NonLinearRealArith | SMT-RAT | 1.036174 | 0.473766 |
| QF_ADT_LinArith | SMTInterpol | 1.014455 | 1.522788 |
| QF_Equality_LinearArith | OpenSMT | 1.013889 | 1.362268 |
| QF_LinearIntArith | OpenSMT | 1.010805 | 0.261748 |
| QF_Bitvec | Bitwuzla | 1.005541 | 1.906713 |
| QF_LinearRealArith | Yices2 | 1.001692 | 1.730295 |
| QF_FPArith | cvc5 | 1.000452 | 0.605873 |
| QF_Equality_Bitvec | Bitwuzla | 1 | 2.205669 |
| QF_Equality | OpenSMT | 1 | 1.297969 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | SMTInterpol | 1.395137 | 1.502915 |
| QF_Equality_NonLinearArith | cvc5 | 1.251773 | 0.829817 |
| QF_ADT_BitVec | Bitwuzla | 1.095348 | 17.675811 |
| QF_NonLinearIntArith | Yices2 | 1.072645 | 35.517632 |
| QF_NonLinearRealArith | SMT-RAT | 1.036174 | 0.479133 |
| QF_ADT_LinArith | SMTInterpol | 1.014455 | 1.997009 |
| QF_Equality_LinearArith | OpenSMT | 1.013889 | 1.046461 |
| QF_LinearIntArith | OpenSMT | 1.010805 | 0.263454 |
| QF_Bitvec | Bitwuzla | 1.005541 | 1.883834 |
| QF_LinearRealArith | Yices2 | 1.001692 | 1.725949 |
| QF_FPArith | cvc5 | 1.000452 | 0.677801 |
| QF_Equality_Bitvec | Bitwuzla | 1 | 2.198479 |
| QF_Equality | OpenSMT | 1 | 1.192156 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Datatypes | SMTInterpol | 1.395137 | 1.502915 |
| QF_Equality_NonLinearArith | cvc5 | 1.251773 | 0.829817 |
| QF_ADT_BitVec | Bitwuzla | 1.095348 | 17.675811 |
| QF_NonLinearIntArith | Yices2 | 1.072645 | 35.517632 |
| QF_NonLinearRealArith | SMT-RAT | 1.036174 | 0.479133 |
| QF_ADT_LinArith | SMTInterpol | 1.014455 | 1.997009 |
| QF_Equality_LinearArith | OpenSMT | 1.013889 | 1.046461 |
| QF_LinearIntArith | OpenSMT | 1.010805 | 0.263454 |
| QF_Bitvec | Bitwuzla | 1.005541 | 1.883834 |
| QF_LinearRealArith | Yices2 | 1.001692 | 1.725949 |
| QF_FPArith | cvc5 | 1.000452 | 0.677801 |
| QF_Equality_Bitvec | Bitwuzla | 1 | 2.198479 |
| QF_Equality | OpenSMT | 1 | 1.192156 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_NonLinearIntArith | Yices2 | 2.17137 | 0.557579 |
| QF_Datatypes | SMTInterpol | 1.479542 | 0.645562 |
| QF_Equality_NonLinearArith | cvc5 | 1.295238 | 0.970407 |
| QF_ADT_BitVec | Bitwuzla | 1.23312 | 3.29299 |
| QF_LinearIntArith | Yices2 | 1.189674 | 1.504684 |
| QF_Equality_Bitvec | Yices2 | 1.043716 | 1.014453 |
| QF_ADT_LinArith | SMTInterpol | 1.036936 | 1.049349 |
| QF_Bitvec | Bitwuzla | 1.033079 | 0.738656 |
| QF_LinearRealArith | Yices2 | 1.030829 | 1.598645 |
| QF_Equality_LinearArith | SMTInterpol | 1.013333 | 0.904105 |
| QF_NonLinearRealArith | SMT-RAT | 1.011994 | 0.876962 |
| QF_FPArith | Bitwuzla | 1.001153 | 1.156261 |
| QF_Equality | OpenSMT | 1 | 1.192156 |