Bitwuzla

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

Ternary Propagation-Based Local Search For More Bit-Precise Reasoning

Aina Niemetz, Mathias Preiner

This site provides our paper Ternary Propagation-Based Local Search For More Bit-Precise Reasoning and related material at FMCAD 2020.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

Paper at FMCAD 2020 (errata)
README for the artifact
Artifact [tar.xz]
Benchmarks [tar.xz]
Bitwuzla Binary [tar.xz]