The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2024-07-08
| 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 | 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 |