SMT-COMP 2023 Results

Competition-Wide Recognitions

Largest Contribution Ranking

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

Biggest Lead Ranking

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

Tracks Summary

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

Divisions

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