Bitwuzla

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

SMT-COMP 2024

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

Divisions Entered

Division Awards

Single Query Track

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

1^st place (gold) in the Bitvec (sat)
1^st place (gold) in the FPArith (sequential, parallel, sat, unsat, 24s)
1^st place (gold) in the QF_Bitvec (sequential, parallel, unsat, 24s)
1^st place (gold) in the QF_Equality+Bitvec (sequential, parallel, sat, unsat)
1^st place (gold) in the QF_FPArith (sequential, parallel, sat, unsat, 24s)

Honorable Mentions:

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

Incremental Track

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

1^st place (gold) in the BitVec (24s)
1^st place (gold) in the Equality+MachineArith (parallel, 24s)
1^st place (gold) in the FPArith (parallel)
1^st place (gold) in the QF_Bitvec (parallel)
1^st place (gold) in the QF_Equality+Bitvec (parallel)
1^st place (gold) in the QF_FPArith (parallel, 24s)

Unsat Core Track

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

1^st place (gold) in the FPArith (sequential, parallel, unsat, 24s)
1^st place (gold) in the QF_Bitvec (sequential, parallel, unsat)
1^st place (gold) in the QF_FPArith (sequential, parallel, unsat, 24s)

Honorable Mentions:

In division Equality+MachineArith:
1^st place in logic AUFBV (sequential, parallel, unsat)
In division QF_Equality+Bitvec:
1^st place in logic QF_ABV (sequential, parallel, unsat, 24s)
1^st place in logic QF_AUFBV (24s)

Model Validation Track

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

1^st place (gold) in the QF_ADT_Bitvec (sequential, parallel, sat, 24s)

Honorable Mentions:

In division QF_FPArith:
  1^st place in logic QF_ABVFP (sequential, parallel, sat, 24s)
  1^st place in logic QF_BVFP (24s)
  1^st place in logic QF_BVFPLRA (sequential, parallel, sat, 24s)
  1^st place in logic QF_FP (24s)
  1^st place in logic QF_FPLRA (sequential, parallel, sat, 24s)

Competition-Wide Awards

Biggest Lead

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

Largest Contribution

2^nd place (silver) in the Incremental Track (parallel)
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 (sequential, parallel, sat)
2^nd place (silver) in the Unsat Core Track (24s)
3^rd place (bronze) in the Unsat Core Track (sequential, parallel, unsat)
3^rd place (bronze) in the Single Query Track (sequential, parallel)