The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2024-07-08
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| OpenSMT | Bitwuzla | - | - | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_LinearRealArith | OpenSMT | 405 | 0.000766 |
| Equality_MachineArith | Bitwuzla | 3.632 | 0.150965 |
| QF_NonLinearIntArith | SMTInterpol | 2.508583 | 3.880798 |
| Equality | cvc5 | 1.827196 | 3.270403 |
| FPArith | Bitwuzla | 1.786458 | 0.18891 |
| Equality_NonLinearArith | cvc5 | 1.501899 | 0.931216 |
| QF_LinearIntArith | Yices2 | 1.38661 | 2.198748 |
| QF_FPArith | Bitwuzla | 1.111141 | 38.701257 |
| Arith | cvc5 | 1.106199 | 1.555787 |
| QF_Equality_Bitvec | Bitwuzla | 1.058689 | 0.441102 |
| QF_Equality_LinearArith | SMTInterpol | 1.046963 | 0.928849 |
| Equality_LinearArith | cvc5 | 1.022814 | 4.928785 |
| QF_Equality_Bitvec_Arith | Yices2 | 1.0094 | 3.979767 |
| QF_Bitvec | Bitwuzla | 1.007578 | 0.98593 |
| QF_Equality_NonLinearArith | cvc5 | 1.006605 | 0.201413 |
| Bitvec | cvc5 | 1.000035 | 0.214001 |
| QF_Equality | Yices2 | 1 | 1.020818 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| Equality_MachineArith | Bitwuzla | 2.771673 | 10.895901 |
| QF_NonLinearIntArith | SMTInterpol | 2.508583 | 3.010001 |
| FPArith | Bitwuzla | 1.644556 | 3.358736 |
| Equality | cvc5 | 1.442037 | 1.728357 |
| Equality_NonLinearArith | cvc5 | 1.39632 | 1.897101 |
| Bitvec | cvc5 | 1.159654 | 0.278373 |
| QF_LinearRealArith | OpenSMT | 1.118162 | 1.411138 |
| QF_LinearIntArith | Yices2 | 1.117873 | 1.853192 |
| QF_FPArith | Bitwuzla | 1.111137 | 18.162984 |
| Arith | cvc5 | 1.085244 | 13.377381 |
| Equality_LinearArith | cvc5 | 1.025558 | 10.07295 |
| QF_Equality_LinearArith | SMTInterpol | 1.015989 | 0.889812 |
| QF_Equality_Bitvec | Bitwuzla | 1.008896 | 1.063066 |
| QF_Equality_NonLinearArith | cvc5 | 1.007407 | 0.044863 |
| QF_Equality_Bitvec_Arith | Yices2 | 1.004577 | 3.935014 |
| QF_Bitvec | Bitwuzla | 1.000307 | 1.169598 |
| QF_Equality | Yices2 | 1 | 1.015162 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_LinearIntArith | Yices2 | 480.536009 | 1.086068 |
| QF_Equality_LinearArith | Yices2 | 2.592321 | 2.535711 |
| Equality | cvc5 | 2.354712 | 0.302926 |
| Equality_NonLinearArith | cvc5 | 2.08308 | 0.323652 |
| QF_FPArith | Bitwuzla | 1.740283 | 2.46326 |
| QF_Equality_NonLinearArith | SMTInterpol | 1.497346 | 1.519868 |
| FPArith | cvc5 | 1.17912 | 3.822455 |
| Arith | SMTInterpol | 1.138715 | 0.780173 |
| Bitvec | Bitwuzla | 1.124359 | 0.90164 |
| Equality_LinearArith | cvc5 | 1.101341 | 0.572284 |
| QF_Equality_Bitvec_Arith | Yices2 | 1.040029 | 1.525832 |
| QF_Equality_Bitvec | Yices2 | 1.006857 | 1.332011 |
| QF_Bitvec | STP | 1.000109 | 0.964146 |
| Equality_MachineArith | Bitwuzla | 1 | 3.340593 |
| QF_Equality | Yices2 | 1 | 1.015162 |