This thesis presents Beaver --- an efficient SMT solver for the quantifier-free fixed-size bit-vector logic (QF_BV). Beaver is an eager solver, that is, given an SMT formula, it first performs word-level simplications and then bitblasts the simplified formula to a Boolean formula, which is then solved using any SAT solver. Several engineering techniques are behind its efficiency: 1) efficient constant/constraint propagation using event-driven approach, 2) several word-level rewrite rules, 3) efficient bitblasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplication techniques of ABC logic synthesis system.

In this thesis, we highlight the implementation details of Beaver that distinguishes it from other solvers. We also present an experimental evaluation and analysis of the effectiveness of our solver against all available QF_BV solvers on the SMT-LIB benchmark suite.

Beaver is an open-source tool implemented in OCaml, usable with any back-end SAT engine, and has a well-documented extensible code base that can be used to experiment with new algorithms and techniques.