The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2025-08-11
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|---|---|---|---|
- | Z3-Parti-Z3pp | Z3-Parti-Z3pp | SMTS | Z3-Parti-Z3pp |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearRealArith | Z3-Parti-Z3pp | 2.125 | 0.01221 |
QF_NonLinearIntArith | Z3-Parti-Z3pp | 2 | 0.479565 |
QF_LinearRealArith | SMTS | 1.642857 | 1.013739 |
QF_Equality_LinearArith | SMTS | 1.454545 | 0.723263 |
QF_Bitvec | STP-Parti-Bitwuzla | 1.272727 | 0.522612 |
QF_LinearIntArith | SMTS | 1.208333 | 1.464977 |
QF_Equality_Bitvec | Bitwuzla | 1.090909 | 1.328785 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearRealArith | Z3-Parti-Z3pp | 3.25 | 0.004461 |
QF_NonLinearIntArith | Z3-Parti-Z3pp | 2.8 | 0.296723 |
QF_Equality_LinearArith | Yices2 | 2.666667 | 0.086862 |
QF_LinearIntArith | SMTS | 1.769231 | 0.59306 |
QF_Bitvec | STP-Parti-Bitwuzla | 1.555556 | 0.398285 |
QF_Equality_Bitvec | Bitwuzla | 1.5 | 0.250215 |
QF_LinearRealArith | SMTS | 1.4 | 1.158349 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_Equality_LinearArith | SMTS | 3.5 | 0.151856 |
QF_LinearRealArith | SMTS | 2 | 0.70265 |
QF_LinearIntArith | Z3-Parti-Z3pp | 1.714286 | 0.306078 |
QF_NonLinearIntArith | Z3-Parti-Z3pp | 1.285714 | 0.858253 |
QF_Equality_Bitvec | Yices2 | 1.142857 | 0.280482 |
QF_Bitvec | STP-Parti-Bitwuzla | 1.071429 | 0.758541 |
QF_NonLinearRealArith | Yices2 | 1 | 39.560568 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearIntArith | Z3-Parti-Z3pp | 3.333333 | 0.356843 |
QF_Equality_Bitvec | Bitwuzla | 2.5 | 0.159304 |
QF_LinearIntArith | SMTS | 2 | 0.677416 |
QF_LinearRealArith | SMTS | 2 | 0.052302 |
QF_Equality_LinearArith | Yices2 | 2 | 0.042071 |
QF_Bitvec | Bitwuzla | 1.666667 | 0.393272 |
QF_NonLinearRealArith | Yices2 | 1.166667 | 1.136855 |