The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2022-08-10 11:17:47 +0000
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 10.61111111 | 1.33300976 | QF_Datatypes |
| cvc5 | 3.26117647 | 0.24590598 | Equality+MachineArith |
| cvc5 | 1.32388664 | 0.54156851 | QF_Equality+NonLinearArith |
| cvc5 | 1.27700312 | 1.56806571 | Equality+NonLinearArith |
| cvc5 | 1.13517034 | 1.84504345 | Equality+LinearArith |
| cvc5 | 1.10313316 | 1.00700477 | Equality |
| Bitwuzla | 1.06714944 | 1.33744351 | FPArith |
| cvc5 | 1.05595829 | 0.83944557 | QF_NonLinearIntArith |
| cvc5 | 1.04280973 | 1.76505711 | QF_Strings |
| cvc5 | 1.0375 | 1.13626308 | Arith |
| cvc5 | 1.02641056 | 1.06771163 | Bitvec |
| cvc5 | 1.02290076 | 1.04675408 | QF_NonLinearRealArith |
| Bitwuzla | 1.01827802 | 2.34307202 | QF_Equality+Bitvec |
| Bitwuzla | 1.00699301 | 1.60149953 | QF_FPArith |
| Yices2 | 1.00670241 | 1.20463539 | QF_LinearRealArith |
| Bitwuzla | 1.00658216 | 1.13385301 | QF_Bitvec |
| OpenSMT | 1.00337937 | 0.92654312 | QF_LinearIntArith |
| smtinterpol | 1.00115075 | 0.80238756 | QF_Equality+LinearArith |
| Yices2 | 1.00026364 | 4.85723832 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 6.82142857 | 1.31907036 | QF_Datatypes |
| cvc5 | 3.26117647 | 0.23920452 | Equality+MachineArith |
| cvc5 | 1.32388664 | 0.54170279 | QF_Equality+NonLinearArith |
| cvc5 | 1.19746341 | 1.36920383 | Equality+NonLinearArith |
| cvc5 | 1.10667188 | 1.5754569 | Equality+LinearArith |
| Bitwuzla | 1.06714944 | 1.35431302 | FPArith |
| cvc5 | 1.05608546 | 0.83244353 | QF_NonLinearIntArith |
| cvc5 | 1.04280973 | 1.75652977 | QF_Strings |
| cvc5 | 1.04192355 | 0.9590123 | Equality |
| cvc5 | 1.0375 | 1.13560198 | Arith |
| cvc5 | 1.02290076 | 1.04771982 | QF_NonLinearRealArith |
| cvc5 | 1.02272727 | 1.00184007 | Bitvec |
| Bitwuzla | 1.01827802 | 2.34323093 | QF_Equality+Bitvec |
| Bitwuzla | 1.00699301 | 1.60013192 | QF_FPArith |
| Bitwuzla | 1.00670486 | 1.1340323 | QF_Bitvec |
| Yices2 | 1.00670241 | 1.20845822 | QF_LinearRealArith |
| OpenSMT | 1.00337937 | 0.92988828 | QF_LinearIntArith |
| smtinterpol | 1.00287687 | 0.90372137 | QF_Equality+LinearArith |
| Yices2 | 1.00026364 | 4.82812457 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 52.0 | 1.17423688 | QF_Datatypes |
| cvc5 | 15.18181818 | 0.56053261 | Equality+MachineArith |
| cvc5 | 6.95412844 | 7.47285582 | Equality+LinearArith |
| cvc5 | 1.74623116 | 5.53191706 | Equality+NonLinearArith |
| cvc5 | 1.24102564 | 0.23525921 | QF_Equality+NonLinearArith |
| cvc5 | 1.13467947 | 0.78356191 | QF_NonLinearIntArith |
| Bitwuzla | 1.07730673 | 1.05141093 | FPArith |
| Z3++ | 1.07148594 | 1.94439792 | QF_NonLinearRealArith |
| cvc5 | 1.05532787 | 0.45071354 | Equality |
| cvc5 | 1.046875 | 2.38456775 | QF_Strings |
| Z3++ | 1.03947368 | 2.02765675 | QF_LinearIntArith |
| smtinterpol | 1.03559871 | 3.42766394 | QF_Equality+LinearArith |
| YicesQS | 1.02893309 | 1.41279484 | Arith |
| Yices2 | 1.01415094 | 1.44617613 | QF_LinearRealArith |
| cvc5 | 1.01310044 | 0.73766873 | Bitvec |
| Bitwuzla | 1.0102209 | 1.27628909 | QF_Bitvec |
| Bitwuzla | 1.00380807 | 2.12877479 | QF_Equality+Bitvec |
| Yices2 | 1.0 | 5.32859641 | QF_Equality |
| Bitwuzla | 1.0 | 2.24140826 | QF_FPArith |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 5.0 | 1.51660306 | QF_Datatypes |
| cvc5 | 2.60643564 | 0.0512143 | Equality+MachineArith |
| cvc5 | 1.62264151 | 0.96520024 | QF_Equality+NonLinearArith |
| Z3++ | 1.12342216 | 2.27291615 | QF_NonLinearIntArith |
| cvc5 | 1.08459596 | 1.3507738 | Arith |
| Bitwuzla | 1.06344951 | 5.397162 | FPArith |
| cvc5 | 1.06204878 | 1.92811964 | Equality+NonLinearArith |
| cvc5 | 1.04373581 | 3.14330573 | Equality+LinearArith |
| Bitwuzla | 1.04302477 | 2.54384758 | QF_Equality+Bitvec |
| cvc5 | 1.03612335 | 1.34111351 | Equality |
| cvc5 | 1.03301016 | 1.62629128 | QF_Strings |
| cvc5 | 1.02631579 | 1.17521467 | Bitvec |
| Yices2 | 1.02138365 | 1.99960048 | QF_Equality+LinearArith |
| cvc5 | 1.01242236 | 1.01757708 | QF_LinearRealArith |
| Bitwuzla | 1.01135074 | 1.57772385 | QF_FPArith |
| cvc5 | 1.00852053 | 0.93044863 | QF_NonLinearRealArith |
| STP | 1.00192493 | 1.16171431 | QF_Bitvec |
| cvc5 | 1.00160128 | 0.78869217 | QF_LinearIntArith |
| Yices2 | 1.00044783 | 4.8107369 | QF_Equality |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 3.19169329 | 0.24291374 | Equality+MachineArith |
| smtinterpol | 2.0 | 1.00065597 | QF_Datatypes |
| cvc5 | 1.57346939 | 1.50193731 | Equality+NonLinearArith |
| cvc5 | 1.28444444 | 0.46588432 | QF_Equality+NonLinearArith |
| Vampire | 1.28359788 | 1.06127243 | Equality |
| cvc5 | 1.23645833 | 1.71964945 | Equality+LinearArith |
| Yices2 | 1.16805959 | 1.92825021 | QF_LinearIntArith |
| Q3B | 1.12150838 | 1.43895702 | Bitvec |
| Bitwuzla | 1.0908414 | 1.29413174 | FPArith |
| Bitwuzla | 1.07785888 | 1.12314096 | QF_FPArith |
| cvc5 | 1.06565513 | 1.79140892 | QF_Strings |
| Yices2 | 1.05067568 | 1.19566082 | QF_LinearRealArith |
| YicesQS | 1.04996097 | 1.28189798 | Arith |
| Yices2 | 1.01808318 | 2.31059772 | QF_Equality+LinearArith |
| Yices2 | 1.01336541 | 8.99546505 | QF_Equality |
| Bitwuzla | 1.00824742 | 1.05308678 | QF_Equality+Bitvec |
| STP | 1.00712965 | 1.37891029 | QF_Bitvec |
| cvc5 | 1.00575476 | 1.03413689 | QF_NonLinearRealArith |
| Yices2 | 1.0 | 1.00001137 | QF_NonLinearIntArith |
n Non-competing.
e Experimental.