The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2021-07-18 17:29:11 +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 | 36.4375 | 1.08879385 | Equality+MachineArith |
| cvc5 | 5.89669421 | 0.10439314 | FPArith |
| Vampire | 1.97598628 | 1.18351416 | Equality+NonLinearArith |
| cvc5 | 1.30319735 | 1.81883207 | Arith |
| cvc5 | 1.20588235 | 0.74281463 | QF_Equality+NonLinearArith |
| cvc5 | 1.18613452 | 8.61367201 | QF_Strings |
| cvc5 | 1.12988827 | 1.55400896 | Bitvec |
| cvc5 | 1.09827899 | 1.54251475 | QF_NonLinearRealArith |
| cvc5 | 1.09425134 | 0.63171573 | QF_FPArith |
| Vampire | 1.08749096 | 0.50550231 | Equality |
| cvc5 | 1.06271543 | 4.95611896 | Equality+LinearArith |
| cvc5 | 1.04891447 | 0.00299378 | QF_Equality |
| cvc5 | 1.04739944 | 1.10809755 | QF_NonLinearIntArith |
| cvc5 | 1.02825456 | 0.8351303 | QF_LinearIntArith |
| Bitwuzla | 1.01278364 | 1.82723063 | QF_Equality+Bitvec |
| SMTInterpol | 1.00954907 | 1.36225986 | QF_Equality+LinearArith |
| Yices2 | 1.00265957 | 1.11646704 | QF_LinearRealArith |
| Bitwuzla | 1.00139551 | 1.06179175 | QF_Bitvec |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 36.4375 | 0.58358606 | Equality+MachineArith |
| cvc5 | 5.89669421 | 0.09376575 | FPArith |
| iProver | 3.75095785 | 0.1288316 | Equality+NonLinearArith |
| cvc5 | 1.30176211 | 1.65845602 | Arith |
| cvc5 | 1.20588235 | 0.7430267 | QF_Equality+NonLinearArith |
| cvc5 | 1.18613452 | 7.89102439 | QF_Strings |
| Vampire | 1.1373825 | 1.08399196 | Equality |
| cvc5 | 1.12988827 | 1.33757622 | Bitvec |
| cvc5 | 1.09827899 | 1.42990955 | QF_NonLinearRealArith |
| cvc5 | 1.09425134 | 0.63233676 | QF_FPArith |
| cvc5 | 1.048092 | 1.42035236 | QF_Equality |
| cvc5 | 1.04739944 | 0.94252848 | QF_NonLinearIntArith |
| cvc5 | 1.03870173 | 2.08500366 | Equality+LinearArith |
| cvc5 | 1.02825456 | 0.83533794 | QF_LinearIntArith |
| Bitwuzla | 1.01278364 | 1.828444 | QF_Equality+Bitvec |
| SMTInterpol | 1.01007958 | 1.57743152 | QF_Equality+LinearArith |
| Yices2 | 1.00265957 | 1.12741395 | QF_LinearRealArith |
| Bitwuzla | 1.00139551 | 1.06262483 | QF_Bitvec |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 11.57142857 | 0.35060571 | Equality+MachineArith |
| cvc5 | 5.21875 | 0.04260596 | FPArith |
| UltimateEliminator+MathSAT | 3.98809524 | 0.02221819 | Equality+NonLinearArith |
| cvc5 | 2.02702703 | 1.99026074 | Equality+LinearArith |
| Vampire | 1.92405063 | 2.94818636 | Equality |
| cvc5 | 1.58035714 | 2.00379437 | Arith |
| cvc5 | 1.28882536 | 13.95658576 | QF_Strings |
| cvc5 | 1.18595041 | 0.28595337 | QF_Equality+NonLinearArith |
| cvc5 | 1.11106766 | 0.98851704 | QF_NonLinearIntArith |
| cvc5 | 1.09864603 | 1.43341685 | QF_NonLinearRealArith |
| cvc5 | 1.04 | 0.78346437 | Bitvec |
| cvc5 | 1.03987241 | 0.49931738 | QF_FPArith |
| cvc5 | 1.02692998 | 1.15012153 | QF_Equality |
| SMTInterpol | 1.01934236 | 5.60462245 | QF_Equality+LinearArith |
| cvc5 | 1.01834431 | 0.86192501 | QF_LinearIntArith |
| Yices2 | 1.01666667 | 1.65369823 | QF_LinearRealArith |
| Bitwuzla | 1.00885236 | 1.3555389 | QF_Bitvec |
| Bitwuzla | 1.00047755 | 2.36157171 | QF_Equality+Bitvec |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 77.0 | 1.5341497 | Equality+MachineArith |
| cvc5 | 6.11173184 | 0.0726739 | FPArith |
| cvc5 | 1.98774259 | 4.01694685 | Equality+NonLinearArith |
| cvc5 | 1.27692308 | 5.81913251 | QF_Equality+NonLinearArith |
| cvc5 | 1.15867159 | 2.1165833 | Bitvec |
| cvc5 | 1.13333333 | 0.6308626 | QF_FPArith |
| cvc5 | 1.09787234 | 2.02745423 | QF_NonLinearRealArith |
| Yices2 | 1.07935872 | 1.37915202 | QF_NonLinearIntArith |
| cvc5 | 1.06299213 | 0.00658011 | QF_Equality |
| Vampire | 1.04447853 | 1.30479335 | Arith |
| cvc5 | 1.04091456 | 0.75761631 | QF_LinearIntArith |
| Bitwuzla | 1.03764479 | 1.79704185 | QF_Equality+Bitvec |
| cvc5 | 1.03204239 | 1.63674716 | QF_Strings |
| cvc5 | 1.02960199 | 3.86513337 | Equality+LinearArith |
| cvc5 | 1.02593918 | 1.2495524 | Equality |
| cvc5 | 1.0152439 | 1.22668029 | QF_LinearRealArith |
| Yices2 | 1.00221198 | 1.05135988 | QF_Bitvec |
| cvc5 | 1.00117509 | 0.86769461 | QF_Equality+LinearArith |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| cvc5 | 32.71428571 | 0.55548247 | Equality+MachineArith |
| cvc5 | 5.36864407 | 0.59548867 | FPArith |
| Yices2 | 1.58681818 | 2.16398387 | QF_LinearIntArith |
| Vampire | 1.56305385 | 1.02611156 | Equality+NonLinearArith |
| cvc5 | 1.38215712 | 1.74459896 | Arith |
| cvc5 | 1.24125874 | 0.75695847 | QF_Equality+NonLinearArith |
| Vampire | 1.23921971 | 1.04554358 | Equality |
| cvc5 | 1.17667436 | 2.46909563 | Equality+LinearArith |
| Yices2 | 1.16903579 | 1.23506502 | QF_NonLinearIntArith |
| cvc5 | 1.16129032 | 2.52091417 | QF_Strings |
| Yices2 | 1.11934901 | 1.32394919 | QF_LinearRealArith |
| cvc5 | 1.06744299 | 1.09721544 | QF_NonLinearRealArith |
| cvc5 | 1.03768116 | 1.01573407 | Bitvec |
| SMTInterpol | 1.03357997 | 0.9876565 | QF_Equality+LinearArith |
| cvc5 | 1.02002861 | 0.46054971 | QF_FPArith |
| Yices2 | 1.00925436 | 32.17364491 | QF_Equality |
| Bitwuzla | 1.00636303 | 1.06889774 | QF_Equality+Bitvec |
| Bitwuzla | 1.00329782 | 0.76419075 | QF_Bitvec |
n Non-competing.
e Experimental.