Bitwuzla

An SMT solver for bit-vectors, floating-points, arrays and uninterpreted functions.

SMT-COMP 2023

Competing Version: submitted binary
System Description: Bitwuzla at the SMT-COMP 2023

Divisions Entered

Division Awards

Single Query Track

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

1^st place (gold) in the Bitvec (sat, 24s)
1^st place (gold) in the FPArith (all)
1^st place (gold) in the QF_Equality+Bitvec (all)
1^st place (gold) in the QF_FPArith (all)

Honorable Mentions:

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

Incremental Track

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

1^st place (gold) in the Equality+MachineArith (all)
1^st place (gold) in the FPArith (all)
1^st place (gold) in the QF_Bitvec (all)
1^st place (gold) in the QF_Equality+Bitvec (all)
1^st place (gold) in the QF_FPArith (all)

Model Validation Track

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

1^st place (gold) in the QF_Equality+Bitvec (all)

Unsat Core Track

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

1^st place (gold) in the FPArith (all)

Honorable Mentions:

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

Competition-Wide Awards

Biggest Lead

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

Largest Contribution

2^nd place (silver) in the Single Query Track (sat)
3^rd place (bronze) in the Single Query Track (sequential, parallel)
3^rd place (bronze) in the Incremental Track (all)
3^rd place (bronze) in the Unsat Core Track (sequential, parallel)