Bitwuzla

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

SMT-COMP 2020

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

Divisions Entered

Single Query Track:
- BV
- QF_ABV
- QF_ABVFP
- QF_AUFBV
- QF_BV
- QF_BVFP
- QF_FP
- QF_UFBV
- QF_UFFP
Incremental Track:
- QF_ABV
- QF_ABVFP
- QF_AUFBV
- QF_BV
- QF_BVFP
- QF_FP
- QF_UFBV
- QF_UFFP
Unsat Core Track:
- QF_ABV
- QF_ABVFP
- QF_AUFBV
- QF_BV
- QF_BVFP
- QF_FP
- QF_UFBV
- QF_UFFP
Model Validation Track:
- QF_BV

Division Awards

Single Query Track

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

1^st place (gold) in the QF_ABV (all)
1^st place (gold) in the QF_ABVFP (all)
1^st place (gold) in the QF_BV (all)
1^st place (gold) in the QF_BVFP (all)
1^st place (gold) in the QF_FP (sequential, parallel, sat, unsat)
1^st place (gold) in the QF_UFBV (24s)
1^st place (gold) in the QF_UFFP (24s)

Incremental Track

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

1^st place (gold) in the QF_ABV (all)
1^st place (gold) in the QF_ABVFP (all)
1^st place (gold) in the QF_BVFP (all)
1^st place (gold) in the QF_UFBV (all)
1^st place (gold) in the QF_UFFP (all)

Model Validation Track

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

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

Unsat Core Track

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

Competition-Wide Awards

Biggest Lead

1^st place (gold) in the Model Validation Track (all)
3^rd place (bronze) in the Incremental Track (all)
3^rd place (bronze) in the Unsat Core Track (all)

Largest Contribution

1^st place (gold) in the Model Validation Track (all)
3^rd place (bronze) in the Incremental Track (all)
3^rd place (bronze) in the Unsat Core Track (all)