cvc5 at SMT-COMP 2023

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

Single Query Track

Results: https://smt-comp.github.io/2023/results/results-single-query
Awards: sequential (seq), parallell (par), sat, unsat, 24s

  1^st place in division Arith (seq, par, unsat)
  1^st place in division Bitvec (seq, par, unsat)
  1^st place in division Equality (seq, par, sat, unsat)
  1^st place in division Equality+LinearArith (all)
  1^st place in division Equality+MachineArith (all)
  1^st place in division Equality+NonLinearArith (seq, par, unsat, 24s)
  1^st place in division QF_Datatypes (seq, par, sat, unsat)
  1^st place in division QF_Equality+NonLinearArith (all)
  1^st place in division QF_LinearIntArith (unsat)
  1^st place in division QF_LinearRealArith (unsat)
  1^st place in division QF_NonLinearRealArith (unsat, 24s)
  1^st place in division QF_Strings (seq, par, sat, unsat)

Honorable Mentions

In division Arith:
  1^st place in logic LIA (sat, 24s)
  1^st place in logic NIA (sat, 24s)

In division Equality:
  1^st place in logic UFDT (24s)

In division QF_Equality+NonLinearArith:
  1^st place in logic QF_UFNIA (sat)

In division QF_FPArith:
  1^st place in logic QF_FP (sat)

In division QF_LinearIntArith:
  1^st place in logic QF_UFDTLIRA (all)

In division QF_NonLinearIntArith:
  1^st place in logic QF_NIRA (seq, par, unsat)

In division QF_Equality+Bitvec:
  1^st place in logic QF_UFBVDT (all)

Incremental Track

Results: https://smt-comp.github.io/2023/results/results-incremental
Awards: parallell (par)

  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+NonLinearArith (all)
  1^st place in division QF_Equality (all)
  1^st place in division QF_Equality+BitVec+Arith (all)
  1^st place in division QF_Equality+NonLinearArith (all)

Honorable Mentions

In division QF_Equality+LinearArith:
  1^st place in logic QF_ALIA (all)

In division QF_FPArith:
  1^st place in logic QF_BVFPLRA (all)

Unsat Core Track

Results: https://smt-comp.github.io/2023/results/results-unsat-core
Awards: sequential (seq), parallell (par)

  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 (seq)
  1^st place in division QF_Equality+NonLinearArith (all)
  1^st place in division QF_FPArith (all)

Honorable Mentions

In division QF_Equality+LinearArith:
  1^st place in logic QF_AUFLIA (all)
  1^st place in logic QF_UFLRA (all)

In division QF_LinearIntArith:
  1^st place in logic QF_IDL (all)
  1^st place in logic QF_UFDTLIRA (all)

Biggest Lead

  1^st place (gold) in the Single Query Track (seq, par, sat, unsat)
  1^st place (gold) in the Unsat Core Track (all)
  2^nd place (silver) in the Single Query Track (24s)

Largest Contribution

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