Bitwuzla at SMT-COMP 2024

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

Single Query Track

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

  1^st place in division Bitvec (sat)
  1^st place in division FPArith (all)
  1^st place in division QF_Bitvec (seq, par, unsat, 24s)
  1^st place in division QF_Equality+Bitvec (seq, par, sat, unsat)
  1^st place in division QF_FPArith (all)

Honorable Mentions

In division Equality+MachineArith:
  1^st place in logic ABVFP (sat)
  1^st place in logic AUFBV (all)
  1^st place in logic AUFBVFP (all)
  1^st place in logic UFBV (24s)

Incremental Track

Results: https://smt-comp.github.io/2024/results/results-incremental
Awards: parallell (par), 24s

  1^st place in division BitVec (24s)
  1^st place in division Equality+MachineArith (all)
  1^st place in division FPArith (par)
  1^st place in division QF_Bitvec (par)
  1^st place in division QF_Equality+Bitvec (par)
  1^st place in division QF_FPArith (all)

Unsat Core Track

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

  1^st place in division FPArith (all)
  1^st place in division QF_Bitvec (seq, par, unsat)
  1^st place in division QF_FPArith (all)

Honorable Mentions

In division Equality+MachineArith:
  1^st place in logic AUFBV (seq, par, unsat)

In division QF_Equality+Bitvec:
  1^st place in logic QF_ABV (all)
  1^st place in logic QF_AUFBV (24s)

Model Validation Track

Results: https://smt-comp.github.io/2024/results/results-model-validation
Awards: sequential (seq), parallell (par), sat, 24s

  1^st place in division QF_ADT_Bitvec (all)

Honorable Mentions

In division QF_FPArith:
  1^st place in logic QF_ABVFP (all)
  1^st place in logic QF_BVFP (24s)
  1^st place in logic QF_BVFPLRA (all)
  1^st place in logic QF_FP (24s)
  1^st place in logic QF_FPLRA (all)

Biggest Lead

  1^st place (gold) in the Incremental Track (par)
  3^rd place (bronze) in the Incremental Track (24s)
  3^rd place (bronze) in the Unsat Core Track (seq, par, unsat)
  3^rd place (bronze) in the Single Query Track (sat, unsat)

Largest Contribution

  2^nd place (silver) in the Incremental Track (par)
  3^rd place (bronze) in the Incremental Track (24s)
  2^nd place (silver) in the Model Validation Track (24s)
  3^rd place (bronze) in the Model Validation Track (seq, par, sat)
  2^nd place (silver) in the Unsat Core Track (24s)
  3^rd place (bronze) in the Unsat Core Track (seq, par, unsat)
  3^rd place (bronze) in the Single Query Track (seq, par)