SMT-COMP 2025 Results

Competition-Wide Recognitions

Best Overall Ranking

• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track

Largest Contribution Ranking

• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track

Biggest Lead Ranking

• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track

Tracks Summary

• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track

Divisions

• Arith
• Incremental Track
• Single Query Track
• Unsat Core Track
• Bitvec
• Incremental Track
• Single Query Track
• Unsat Core Track
• Equality
• Incremental Track
• Single Query Track
• Unsat Core Track
• Equality+LinearArith
• Incremental Track
• Single Query Track
• Unsat Core Track
• Equality+MachineArith
• Incremental Track
• Single Query Track
• Unsat Core Track
• Equality+NonLinearArith
• Incremental Track
• Single Query Track
• Unsat Core Track
• FPArith
• Incremental Track
• Single Query Track
• Unsat Core Track
• QF_ADT+BitVec
• Model Validation Track
• QF_ADT+LinArith
• Model Validation Track
• QF_Bitvec
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_Datatypes
• Model Validation Track
• Single Query Track
• Unsat Core Track
• QF_Equality
• Incremental Track
• Model Validation Track
• Single Query Track
• Unsat Core Track
• QF_Equality+Bitvec
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_Equality+Bitvec+Arith
• Incremental Track
• QF_Equality+LinearArith
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_Equality+NonLinearArith
• Incremental Track
• Model Validation Track
• Single Query Track
• Unsat Core Track
• QF_FPArith
• Incremental Track
• Model Validation Track
• Single Query Track
• Unsat Core Track
• QF_LinearIntArith
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_LinearRealArith
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_NonLinearIntArith
• Incremental Track
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_NonLinearRealArith
• Model Validation Track
• Parallel Track
• Single Query Track
• Unsat Core Track
• QF_Strings
• Single Query Track