The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2023-07-06 16:04:55 +0000
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | SMTInterpol |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 2.69117647 | 0.31444117 | QF_Datatypes |
| cvc5 | 2.14190094 | 0.26854389 | Equality+MachineArith |
| cvc5 | 1.9954023 | 0.27808461 | Equality |
| cvc5 | 1.2795501 | 3.84200404 | Equality+NonLinearArith |
| Bitwuzla | 1.14866667 | 1.78526932 | FPArith |
| cvc5 | 1.11956732 | 4.6232174 | Equality+LinearArith |
| cvc5 | 1.11799762 | 0.31324752 | Bitvec |
| Bitwuzla | 1.10166799 | 1.88500677 | QF_FPArith |
| Z3++ | 1.06208143 | 1.14707809 | QF_NonLinearIntArith |
| cvc5 | 1.03965393 | 0.12794489 | Arith |
| Z3++ | 1.03208773 | 1.63505971 | QF_NonLinearRealArith |
| Bitwuzla | 1.03205531 | 1.52493726 | QF_Equality+Bitvec |
| STP | 1.02380705 | 1.33003844 | QF_Bitvec |
| SMTInterpol | 1.02086858 | 0.77737105 | QF_Equality+LinearArith |
| cvc5 | 1.01770536 | 0.36431018 | QF_Strings |
| cvc5 | 1.01078167 | 0.68523936 | QF_Equality+NonLinearArith |
| Yices2 | 1.00267738 | 1.08307991 | QF_LinearRealArith |
| Z3++ | 1.00051573 | 1.23097933 | QF_LinearIntArith |
| Yices2 | 1.0 | 9.64756007 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 5.04651163 | 0.03681285 | Equality |
| cvc5 | 2.14190094 | 0.25487605 | Equality+MachineArith |
| cvc5 | 2.12790698 | 0.43615457 | QF_Datatypes |
| cvc5 | 1.32905297 | 0.57395656 | Equality+LinearArith |
| cvc5 | 1.19408397 | 2.40938472 | Equality+NonLinearArith |
| Bitwuzla | 1.14866667 | 1.8574218 | FPArith |
| cvc5 | 1.11799762 | 0.30335546 | Bitvec |
| Bitwuzla | 1.10166799 | 1.88699216 | QF_FPArith |
| Z3++ | 1.06208143 | 1.14739058 | QF_NonLinearIntArith |
| cvc5 | 1.03965393 | 0.12775416 | Arith |
| Bitwuzla | 1.03205531 | 1.53136925 | QF_Equality+Bitvec |
| Z3++ | 1.0316687 | 1.65750935 | QF_NonLinearRealArith |
| SMTInterpol | 1.02481669 | 0.87618137 | QF_Equality+LinearArith |
| STP | 1.02380705 | 1.32799548 | QF_Bitvec |
| cvc5 | 1.01770536 | 0.35726978 | QF_Strings |
| cvc5 | 1.01078167 | 0.6826328 | QF_Equality+NonLinearArith |
| Yices2 | 1.00267738 | 1.08238011 | QF_LinearRealArith |
| Z3++ | 1.00051573 | 1.23128988 | QF_LinearIntArith |
| Yices2 | 1.0 | 9.53436981 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 2.48339483 | 0.09123091 | Equality+MachineArith |
| cvc5 | 1.7470726 | 0.39855775 | Equality+NonLinearArith |
| Bitwuzla | 1.43358396 | 1.71073895 | FPArith |
| cvc5 | 1.32113145 | 0.00932122 | Equality+LinearArith |
| cvc5 | 1.17073171 | 0.58459303 | QF_Datatypes |
| Z3++ | 1.07444169 | 0.44697523 | QF_NonLinearRealArith |
| Bitwuzla | 1.06947368 | 1.36848337 | QF_FPArith |
| SMTInterpol | 1.06639839 | 0.70776294 | QF_Equality+LinearArith |
| Yices2 | 1.05474453 | 1.20112372 | QF_Equality+NonLinearArith |
| cvc5 | 1.0515873 | 0.11062347 | Equality |
| Z3++ | 1.04973894 | 2.13546305 | QF_LinearIntArith |
| Bitwuzla | 1.03643725 | 9.69117839 | Bitvec |
| YicesQS | 1.03090909 | 4.42529665 | Arith |
| cvc5 | 1.0239389 | 0.42055441 | QF_Strings |
| Z3++ | 1.0157168 | 1.60160178 | QF_NonLinearIntArith |
| Bitwuzla | 1.01506024 | 1.07358409 | QF_Equality+Bitvec |
| OpenSMT | 1.00478469 | 0.67724911 | QF_LinearRealArith |
| STP | 1.00020951 | 1.25125017 | QF_Bitvec |
| Yices2 | 1.0 | 5.40729123 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 3.84394904 | 0.25780422 | Equality |
| cvc5 | 2.95652174 | 0.38523399 | QF_Datatypes |
| cvc5 | 1.94549266 | 0.48051246 | Equality+MachineArith |
| cvc5 | 1.24887244 | 1.70207457 | Equality+LinearArith |
| cvc5 | 1.22891566 | 0.08968687 | QF_Equality+NonLinearArith |
| Bitwuzla | 1.12101911 | 2.09019982 | QF_FPArith |
| cvc5 | 1.08769793 | 0.07760438 | Arith |
| cvc5 | 1.06625578 | 0.24405462 | Bitvec |
| Bitwuzla | 1.06040268 | 2.19488234 | QF_Equality+Bitvec |
| cvc5 | 1.0519084 | 2.9478033 | Equality+NonLinearArith |
| STP | 1.04703941 | 1.38479793 | QF_Bitvec |
| Bitwuzla | 1.04537205 | 2.02194395 | FPArith |
| Z3++ | 1.01484169 | 0.9168849 | QF_NonLinearIntArith |
| cvc5 | 1.01446945 | 0.56211343 | QF_NonLinearRealArith |
| cvc5 | 1.01204819 | 1.06089298 | QF_LinearRealArith |
| cvc5 | 1.0105553 | 0.54143957 | QF_LinearIntArith |
| cvc5 | 1.00584909 | 0.11534775 | QF_Strings |
| OpenSMT | 1.00515464 | 0.61290967 | QF_Equality+LinearArith |
| Yices2 | 1.0 | 9.95933819 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| SMTInterpol | 5.0 | 0.13134389 | QF_Datatypes |
| cvc5 | 1.92173913 | 1.02398014 | Equality+MachineArith |
| cvc5 | 1.5953263 | 2.16400539 | Equality+NonLinearArith |
| cvc5 | 1.26755152 | 2.39933549 | Equality+LinearArith |
| Vampire | 1.21970443 | 0.35182049 | Equality |
| Yices2 | 1.19973603 | 1.99811828 | QF_LinearIntArith |
| Bitwuzla | 1.19274376 | 1.78888553 | FPArith |
| Bitwuzla | 1.08614865 | 1.17840006 | QF_FPArith |
| cvc5 | 1.07590759 | 0.42093019 | QF_Equality+NonLinearArith |
| Yices2 | 1.06304729 | 1.37374749 | QF_LinearRealArith |
| STP | 1.05290645 | 1.86477597 | QF_Bitvec |
| YicesQS | 1.04354469 | 1.6088532 | Arith |
| Z3++ | 1.0328862 | 0.61124157 | QF_NonLinearIntArith |
| Bitwuzla | 1.01710526 | 1.37197059 | Bitvec |
| cvc5 | 1.01390821 | 0.85123034 | QF_NonLinearRealArith |
| Yices2 | 1.01146651 | 7.76599884 | QF_Equality+LinearArith |
| Yices2 | 1.0094086 | 7.87825351 | QF_Equality |
| z3-alpha | 1.00836191 | 0.45199308 | QF_Strings |
| Bitwuzla | 1.00761246 | 0.36810776 | QF_Equality+Bitvec |
n Non-competing.
e Experimental.