SMT-COMP 2024

https://smt-comp.github.io/2024

System Description:  cvc5 at the SMT Competition 2024
Submitted Binaries:

• All Tracks

Divisions Entered

Single Query Track

• Arith
• Bitvec
• Equality
• Equality_LinearArith
• Equality_MachineArith
• Equality_NonLinearArith
• FPArith
• QF_Bitvec
• QF_Datatypes
• QF_Equality
• QF_Equality_Bitvec
• QF_Equality_LinearArith
• QF_Equality_NonLinearArith
• QF_FPArith
• QF_LinearIntArith
• QF_LinearRealArith
• QF_NonLinearIntArith
• QF_NonLinearRealArith
• QF_Strings

Incremental Track

• Arith
• Bitvec
• Equality
• Equality_LinearArith
• Equality_MachineArith
• Equality_NonLinearArith
• FPArith
• QF_Bitvec
• QF_Equality
• QF_Equality_Bitvec
• QF_Equality_Bitvec_Arith
• QF_Equality_LinearArith
• QF_Equality_NonLinearArith
• QF_FPArith
• QF_LinearIntArith
• QF_LinearRealArith
• QF_NonLinearIntArith

Unsat Core Track

• Arith
• Bitvec
• Equality
• Equality_LinearArith
• Equality_MachineArith
• Equality_NonLinearArith
• FPArith
• QF_Bitvec
• QF_Datatypes
• QF_Equality
• QF_Equality_Bitvec
• QF_Equality_LinearArith
• QF_Equality_NonLinearArith
• QF_FPArith
• QF_LinearIntArith
• QF_LinearRealArith
• QF_NonLinearIntArith
• QF_NonLinearRealArith
• QF_Strings

Model Validation Track

• QF_ADT_BitVec
• QF_ADT_LinArith
• QF_Bitvec
• QF_Datatypes
• QF_Equality
• QF_Equality_Bitvec
• QF_Equality_LinearArith
• QF_Equality_NonLinearArith
• QF_FPArith
• QF_LinearIntArith
• QF_LinearRealArith
• QF_NonLinearIntArith
• QF_NonLinearRealArith

Division Awards

Single Query Track

https://smt-comp.github.io/2024/results/results-single-query

  1^st place in division Arith (sequential, parallel, unsat)
  1^st place in division Bitvec (sequential, parallel, unsat)
  1^st place in division Equality (all)
  1^st place in division Equality_LinearArith (all)
  1^st place in division Equality_MachineArith (all)
  1^st place in division Equality_NonLinearArith (all)
  1^st place in division QF_Datatypes (sat)
  1^st place in division QF_Equality_NonLinearArith (unsat)
  1^st place in division QF_LinearIntArith (unsat)
  1^st place in division QF_LinearRealArith (unsat)
  1^st place in division QF_NonLinearRealArith (unsat)

Incremental Track

https://smt-comp.github.io/2024/results/results-incremental

  1^st place in division Arith (parallel)
  1^st place in division Bitvec (parallel)
  1^st place in division Equality (all)
  1^st place in division Equality_LinearArith (all)
  1^st place in division Equality_NonLinearArith (all)
  1^st place in division FPArith (24s)
  1^st place in division QF_Equality_NonLinearArith (parallel)

Unsat Core Track

https://smt-comp.github.io/2024/results/results-unsat-core

  1^st place in division Arith (all)
  1^st place in division Bitvec (all)
  1^st place in division Equality (all)
  1^st place in division Equality_LinearArith (all)
  1^st place in division Equality_MachineArith (all)
  1^st place in division Equality_NonLinearArith (all)
  1^st place in division QF_Datatypes (sequential, parallel, unsat)
  1^st place in division QF_Equality_Bitvec (sequential, parallel, unsat)
  1^st place in division QF_Equality_NonLinearArith (sequential, parallel, unsat)
  1^st place in division QF_NonLinearIntArith (all)
  1^st place in division QF_NonLinearRealArith (all)
  1^st place in division QF_Strings (all)

Model Validation Track

https://smt-comp.github.io/2024/results/results-model-validation

  1^st place in division QF_Equality_NonLinearArith (all)
  1^st place in division QF_FPArith (all)

Biggest Lead

  1^st place (gold) in the Single Query Track (all)
  2^nd place (silver) in the Incremental Track (24s)
  3^rd place (bronze) in the Incremental Track (parallel)
  1^st place (gold) in the Unsat Core Track (all)
  3^rd place (bronze) in the Model Validation Track (24s)

Largest Contribution

  1^st place (gold) in the Single Query Track (all)
  2^nd place (silver) in the Unsat Core Track (sequential, parallel, unsat)
  3^rd place (bronze) in the Unsat Core Track (24s)