cvc5 at SMT-COMP 2021

https://smt-comp.github.io/2021
https://cvc5.github.io

Single Query Track

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

  1^st place in division Arith (sequential, parallel, sat, 24s)
  1^st place in division Bitvec (all)
  1^st place in division Equality+LinearArith (all)
  1^st place in division Equality+MachineArith (all)
  1^st place in division Equality+NonLinearArith (unsat)
  1^st place in division Equality (unsat)
  1^st place in division FPArith (all)
  1^st place in division QF_Equality+LinearArith (unsat)
  1^st place in division QF_Equality+NonLinearArith (all)
  1^st place in division QF_Equality (sequential, parallel, sat, unsat)
  1^st place in division QF_FPArith (all)
  1^st place in division QF_LinearIntArith (sequential, parallel, sat, unsat)
  1^st place in division QF_LinearRealArith (unsat)
  1^st place in division QF_NonLinearIntArith (sequential, parallel, sat)
  1^st place in division QF_NonLinearRealArith (all)
  1^st place in division QF_Strings (all)

Incremental Track

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

  1^st place in division Arith (all)
  1^st place in division Bitvec (all)
  1^st place in division Equality+LinearArith (all)
  1^st place in division Equality (all)
  1^st place in division FPArith (all)
  1^st place in division QF_Equality+LinearArith (all)
  1^st place in division QF_Equality (all)

Model Validation Track

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

  1^st place in division QF_LinearIntArith (all)

Unsat Core Track

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

  1^st place in division Arith (all)
  1^st place in division Bitvec (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 Equality (all)
  1^st place in division FPArith (all)
  1^st place in division QF_Equality+NonLinearArith (all)
  1^st place in division QF_Equality (all)
  1^st place in division QF_LinearIntArith (all)
  1^st place in division QF_NonLinearIntArith (all)
  1^st place in division QF_NonLinearRealArith (all)

Biggest Lead

  1^st place (gold) in the Incremental Track (all)
  1^st place (gold) in the Model Validation Track (all)
  1^st place (gold) in the Single Query Track (all)
  1^st place (gold) in the Unsat Core Track (all)

Largest Contribution

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