The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2024-07-08
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|---|---|---|---|
Yices2 | Yices2 | Yices2 | - | Yices2 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearIntArith | Yices2 | 0.017741 | 0.04685 |
QF_NonLinearRealArith | SMT-RAT | 0.007074 | -0.010048 |
QF_ADT_BitVec | Bitwuzla | 0.003837 | 0.088895 |
QF_NonLinearIntArith | cvc5 | 0.00272 | -0.013181 |
QF_LinearIntArith | OpenSMT | 0.001298 | 0.004351 |
QF_LinearIntArith | cvc5 | 0.001033 | 0.038615 |
QF_Equality_NonLinearArith | cvc5 | 0.001022 | 0.00038 |
QF_LinearIntArith | SMTInterpol | 0.000673 | -0.007798 |
QF_NonLinearRealArith | cvc5 | 0.000591 | 0.005975 |
QF_Equality_NonLinearArith | SMTInterpol | 0.000584 | 0.002248 |
QF_LinearIntArith | Yices2 | 0.000529 | 0.066656 |
QF_Bitvec | Bitwuzla | 0.000257 | 0.036774 |
QF_Equality_LinearArith | OpenSMT | 0.000249 | 0.0159 |
QF_LinearRealArith | OpenSMT | 0.00015 | -0.000272 |
QF_NonLinearRealArith | Yices2 | 0.000115 | 0.017733 |
QF_ADT_BitVec | cvc5 | 0.000107 | 0.007818 |
QF_Bitvec | STP | 8.6e-05 | 0.038246 |
QF_LinearRealArith | Yices2 | 7.5e-05 | 0.007234 |
QF_Equality_NonLinearArith | Yices2 | 6.1e-05 | 0.003221 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearIntArith | Yices2 | 0.017741 | 0.046715 |
QF_NonLinearRealArith | SMT-RAT | 0.007074 | -0.010001 |
QF_ADT_BitVec | Bitwuzla | 0.003837 | 0.0883 |
QF_NonLinearIntArith | cvc5 | 0.00272 | -0.01328 |
QF_LinearIntArith | OpenSMT | 0.001297 | 0.004203 |
QF_LinearIntArith | cvc5 | 0.001032 | 0.038218 |
QF_Equality_NonLinearArith | cvc5 | 0.001022 | 0.00035 |
QF_LinearIntArith | SMTInterpol | 0.000768 | -0.004234 |
QF_NonLinearRealArith | cvc5 | 0.000591 | 0.005813 |
QF_Equality_NonLinearArith | SMTInterpol | 0.000584 | 0.002812 |
QF_LinearIntArith | Yices2 | 0.000528 | 0.062471 |
QF_Bitvec | Bitwuzla | 0.000257 | 0.036063 |
QF_Equality_LinearArith | OpenSMT | 0.000224 | 0.014385 |
QF_LinearRealArith | OpenSMT | 0.00015 | -0.000783 |
QF_NonLinearRealArith | Yices2 | 0.000115 | 0.016933 |
QF_ADT_BitVec | cvc5 | 0.000107 | 0.003391 |
QF_Bitvec | STP | 8.6e-05 | 0.037543 |
QF_LinearRealArith | Yices2 | 7.5e-05 | 0.007203 |
QF_Equality_NonLinearArith | Yices2 | 6.1e-05 | 0.003342 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearIntArith | Yices2 | 0.017741 | 0.046715 |
QF_NonLinearRealArith | SMT-RAT | 0.007074 | -0.010001 |
QF_ADT_BitVec | Bitwuzla | 0.003837 | 0.0883 |
QF_NonLinearIntArith | cvc5 | 0.00272 | -0.01328 |
QF_LinearIntArith | OpenSMT | 0.001297 | 0.004203 |
QF_LinearIntArith | cvc5 | 0.001032 | 0.038218 |
QF_Equality_NonLinearArith | cvc5 | 0.001022 | 0.00035 |
QF_LinearIntArith | SMTInterpol | 0.000768 | -0.004234 |
QF_NonLinearRealArith | cvc5 | 0.000591 | 0.005813 |
QF_Equality_NonLinearArith | SMTInterpol | 0.000584 | 0.002812 |
QF_LinearIntArith | Yices2 | 0.000528 | 0.062471 |
QF_Bitvec | Bitwuzla | 0.000257 | 0.036063 |
QF_Equality_LinearArith | OpenSMT | 0.000224 | 0.014385 |
QF_LinearRealArith | OpenSMT | 0.00015 | -0.000783 |
QF_NonLinearRealArith | Yices2 | 0.000115 | 0.016933 |
QF_ADT_BitVec | cvc5 | 0.000107 | 0.003391 |
QF_Bitvec | STP | 8.6e-05 | 0.037543 |
QF_LinearRealArith | Yices2 | 7.5e-05 | 0.007203 |
QF_Equality_NonLinearArith | Yices2 | 6.1e-05 | 0.003342 |
Division | Solver | Correct Score | Time Score |
---|---|---|---|
QF_NonLinearIntArith | Yices2 | 0.02784 | 0.014387 |
QF_ADT_BitVec | Bitwuzla | 0.018273 | 0.066433 |
QF_LinearIntArith | Yices2 | 0.012468 | 0.05415 |
QF_NonLinearRealArith | SMT-RAT | 0.007083 | -0.009207 |
QF_LinearIntArith | cvc5 | 0.003361 | 0.010069 |
QF_NonLinearIntArith | cvc5 | 0.003195 | 0.001276 |
QF_Bitvec | STP | 0.00177 | 0.000756 |
QF_LinearIntArith | OpenSMT | 0.00138 | -0.005957 |
QF_Bitvec | Bitwuzla | 0.001335 | 0.013555 |
QF_Equality_NonLinearArith | cvc5 | 0.001225 | -0.000308 |
QF_Equality_LinearArith | OpenSMT | 0.001041 | -0.009148 |
QF_Bitvec | Yices2 | 0.001016 | 0.052587 |
QF_LinearRealArith | Yices2 | 0.000837 | 0.00324 |
QF_Equality_NonLinearArith | SMTInterpol | 0.000706 | -0.000227 |
QF_NonLinearRealArith | cvc5 | 0.0007 | -0.003616 |
QF_Equality_NonLinearArith | Yices2 | 0.000576 | -0.000482 |
QF_NonLinearRealArith | Yices2 | 0.000533 | 0.003357 |
QF_LinearIntArith | SMTInterpol | 0.000401 | -0.005258 |
QF_Equality_Bitvec | Yices2 | 0.000394 | 0.001612 |